let compare = DiscriminationTactics.compare_tac
let constructor = IntroductionTactics.constructor_tac
let contradiction = NegationTactics.contradiction_tac
let cut = PrimitiveTactics.cut_tac
let decide_equality = DiscriminationTactics.decide_equality_tac
let decompose = EliminationTactics.decompose_tac
let compare = DiscriminationTactics.compare_tac
let constructor = IntroductionTactics.constructor_tac
let contradiction = NegationTactics.contradiction_tac
let cut = PrimitiveTactics.cut_tac
let decide_equality = DiscriminationTactics.decide_equality_tac
let decompose = EliminationTactics.decompose_tac