let normalize = ReductionTactics.normalize_tac
let reduce = ReductionTactics.reduce_tac
let reflexivity = Setoids.setoid_reflexivity_tac
-let rename = ProofEngineStructuralRules.rename
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac