let decompose = EliminationTactics.decompose_tac
let discriminate = DiscriminationTactics.discriminate_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
let decompose = EliminationTactics.decompose_tac
let discriminate = DiscriminationTactics.discriminate_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac