let absurd = NegationTactics.absurd_tac
let apply = PrimitiveTactics.apply_tac
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
let absurd = NegationTactics.absurd_tac
let apply = PrimitiveTactics.apply_tac
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac