val elim_intros_tac:
term: Cic.term -> ProofEngineTypes.tactic
-val elim_intros_tac:
- term: Cic.term -> ProofEngineTypes.tactic
-
val change_tac:
- what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic
+ what: Cic.term -> with_what: Cic.term -> pattern:ProofEngineTypes.pattern ->
+ ProofEngineTypes.tactic