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
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic