tuned;

clarified type Indexname, with plain value Int;
eliminated pointless cache_int;

tuned header;

tuned output;

more general cache, also for term substructures;