Proper theorem names at last, no fakes!! Added set_prover function to set various parameters to improve success rate. Fixed the auto settings for E.

some corrections

adjusted title

simplified dest_eq; do not export debuging stuff; has_tvars: actually check all types within a term, not just its resulting type; tuned;

commented out parts which have been inactive (unintentionally) for a long time;

removed obsolete dest_eq_typ;

tuned hypsubst setup;