val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
-val let1 : string -> Cic.term -> Cic.term -> ProofEngineTypes.tactic
+val existselim :
+ Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
-val bywehave :
- Cic.term option -> Cic.term -> string -> Cic.term -> string ->
- ProofEngineTypes.tactic
+val andelim :
+ Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
-val prova :
- Cic.term option -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic
+val rewritingstep :
+ Cic.term option -> Cic.term -> Cic.term option -> Cic.name option ->
+ ProofEngineTypes.tactic