* http://cs.unibo.it/helm/.
*)
-val reflexivity_tac: ProofEngineTypes.tactic
-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 right_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 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