val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic
val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
-
-(* FG *)
-
-(* rewrites and clears all simple equalities in the context *)
-val subst_tac: ProofEngineTypes.tactic