val symmetry_tac: ProofEngineTypes.tactic
val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
+(*
val constructor_tac: n:int -> ProofEngineTypes.tactic
+*)
val exists_tac: ProofEngineTypes.tactic
val split_tac: ProofEngineTypes.tactic
val left_tac: ProofEngineTypes.tactic
val assumption_tac: ProofEngineTypes.tactic
+val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic
+
+val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
+
+val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic
+val contradiction_tac: ProofEngineTypes.tactic
+
+val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic
+
(*
-val generalize_tac: Cic.term -> ProofEnginrTypes.tactic
+val decide_equality_tac: ProofEngineTypes.tactic
+val compare_tac: term1:Cic.term -> term2:Cic.term -> ProofEngineTypes.tactic
*)
+
+val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
+val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
+val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic
+val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic