Dnet Dn Btermdn Tacticals Hipattern Ind_tables Eqschemes Elimschemes Tactics Abstract Elim Equality Contradiction Inv Leminv Hints Auto Eauto Class_tactics Term_dnet Eqdecide Autorewrite