"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
"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