let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
let contradiction = NegationTactics.contradiction_tac
let cut = PrimitiveTactics.cut_tac
let decompose = EliminationTactics.decompose_tac
let contradiction = NegationTactics.contradiction_tac
let cut = PrimitiveTactics.cut_tac
let decompose = EliminationTactics.decompose_tac
let destruct = DiscriminationTactics.destruct_tac
let elim_intros = PrimitiveTactics.elim_intros_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
let destruct = DiscriminationTactics.destruct_tac
let elim_intros = PrimitiveTactics.elim_intros_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
let letin = PrimitiveTactics.letin_tac
let normalize = ReductionTactics.normalize_tac
let reduce = ReductionTactics.reduce_tac
let letin = PrimitiveTactics.letin_tac
let normalize = ReductionTactics.normalize_tac
let reduce = ReductionTactics.reduce_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac