proposition: Lemma horpo_args_subst : forall M Ms Ns G (MG: correct_subst M G), subst_list Ms Ns G -> (forall L R (CL: correct_subst L G) (CR: correct_subst R G), (subterm L M \/ (L = M /\ In R Ms)) -> L >> R -> subst CL >> subst CR) -> M [>>] Ms -> subst MG [>>] Ns.
proof: Proof. induction Ms; intros Ns G MG MsNs IH MMs. inversion MsNs. constructor 1. inversion MsNs. assert (rest: subst MG [>>] ys). apply IHMs. inversion MMs; trivial. intros. apply IH; trivial. inversion H4. left; trivial. right; inversion H6; auto with datatypes. inversion MMs; trivial. inversion H1. inversion MMs. constructor 2; trivial. rewrite H4. apply IH; trivial. auto with datatypes. constructor 3; trivial. destruct H8 as [Marg Marg_arg Marg_a]. destruct (subst_arg Marg MG Marg_arg) as [M'arg [M'arg_arg [MargG M'argG]]]. exists M'arg; trivial. inversion Marg_a. constructor. rewrite M'argG, H4. apply IH; trivial. left; apply arg_subterm; trivial. replace M'arg with y. constructor 2. rewrite M'argG, H4. apply term_eq. autorewrite with terms; rewrite H10; trivial. autorewrite with terms; rewrite H10; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)