- "reflexivity", EqualityTactics.reflexivity_tac ;
- "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
- "exact sym_eqt su t1 ...", exact_tac
+ EqualityTactics.reflexivity_tac ;
+ exact_tac ~term:t1'_eq_t1'' ;
+ exact_tac ~term:t2'_eq_t2'' ;
+ exact_tac