proposition: Lemma horpo_subst_stable : forall M N G (MS: correct_subst M G) (NS: correct_subst N G), algebraicSubstitution G -> M >> N -> subst MS >> subst NS.
proof: Proof. intros M N. assert (Res: forall P G (MS: correct_subst (fst P) G) (NS: correct_subst (snd P) G), algebraicSubstitution G -> fst P >> snd P -> subst MS >> subst NS). intro P. apply well_founded_ind with (R := LexProd_Lt) (P := fun P => forall G (MS: correct_subst (fst P) G) (NS: correct_subst (snd P) G), algebraicSubstitution G -> fst P >> snd P -> subst MS >> subst NS). apply lexprod_wf. unfold ltL, gtR, subterm_gt. rewrite transp_invol. apply subterm_wf. unfold ltR, gtR, subterm_gt. rewrite transp_invol. apply subterm_wf. clear M N P. intros P IH G MG NG Gnorm MN. destruct P as [M N]; simpl in * . apply horpo_subst_stable_aux; trivial. intros. apply (IH (L, R)); trivial. destruct H0. constructor; exact H0. destruct H0; rewrite H0. constructor 2; trivial. auto with sets. intros. apply (Res (M, N) G); trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)