ProofEngineTypes.apply_tactic
(P.change_tac
~what:new_t1'
+ ~pattern:([],None)
~with_what:
(C.Appl [
C.Lambda (
))
~continuation:
(T.then_
- ~start:(EqualityTactics.rewrite_simpl_tac ~term)
+ ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
~continuation:EqualityTactics.reflexivity_tac
)
])
~start:
(P.change_tac
~what:gty'
+ ~pattern:([],None)
~with_what:
(C.Appl [
C.Lambda (
~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')