let reflexivity = Setoids.setoid_reflexivity_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
let reflexivity = Setoids.setoid_reflexivity_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac