fact: Variable R_subst_stable : forall M N G (MS: correct_subst M G) (NS: correct_subst N G), algebraicSubstitution G -> M -R-> N -> subst MS -R-> subst NS.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)