Cic.term option -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic
val andelim :
Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
val rewritingstep :
Cic.term option -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic
val andelim :
Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
val rewritingstep :