tuned proofs;

retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;

recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory

in a local context, also the free variable case needs to be analysed default tip

speed-up proof;