more official session qualifier;

clarified;

replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace

merged

clarified output;

more tooltips;

clarified imports;

update strictly local imports only;

proper imports_base;

tuned;