))
~continuation:
(T.then_
- ~start:(EqualityTactics.rewrite_simpl_tac ~term)
+ ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
~continuation:EqualityTactics.reflexivity_tac
)
])
~continuation:
(
T.then_
- ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
+ ~start:(EqualityTactics.rewrite_back_simpl_tac
+ ~term ())
~continuation:(IntroductionTactics.constructor_tac ~n:1)
))
(proof',goal')