proposition: Lemma R_conv_to : forall M N M', M -R-> N -> M ~ M' -> exists N', M' -R-> N' /\ N ~ N'.
proof: Proof. intros. destruct H0. destruct (envSub_min_ex H0) as [x' [MM' [x'min xx']]]. destruct (term_build_conv_sim N MM') as [N' [M'N' NN']]; trivial. apply R_env_preserving; trivial. apply R_var_consistent; trivial. exists N'; split. apply R_conv_comp with M N x'; trivial. exists x'; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)