let left = IntroductionTactics.left_tac
let letin = PrimitiveTactics.letin_tac
let normalize = ReductionTactics.normalize_tac
-let reduce = ReductionTactics.reduce_tac
let reflexivity = Setoids.setoid_reflexivity_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac