shortcut binary minimization algorithm

speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half

renamed experimental systems

repaired quantification over type variables for non-TFF1/THF encodings

misc tuning and modernization; more antiquotations;

misc tuning and modernization; more antiquotations;

tuned;

some statespace benchmarks;

write changed .prv files only, to avoid writing into src file-space by default;

tuned document; tuned proofs;

more precise dependencies;

inlined antiquotations;

misc tuning and modernization;

optional timing, to avoid redundant allocation of mutable cells;

tuned;