val replace_tac:
pattern:ProofEngineTypes.pattern ->
- with_what:Cic.term -> ProofEngineTypes.tactic
+ with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic