let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
-let set_goal = ProofEngineStructuralRules.set_goal
let simpl = ReductionTactics.simpl_tac
let split = IntroductionTactics.split_tac
let subst = SubstTactic.subst_tac