proposition: Lemma horpo_args_conv : forall M N Ms Ns Q, M ~(Q) N -> (forall MsX, In MsX Ms -> env MsX = env M) -> (forall NsX, In NsX Ns -> env NsX = env N) -> conv_list Ms Ns Q -> (forall L L' R R', (subterm L M \/ (L = M /\ In R Ms)) -> L ~(Q) L' -> R ~(Q) R' -> L >> R -> env L' = env R' -> L' >> R' ) -> M [>>] Ms -> N [>>] Ns.
proof: Proof. induction Ms; intros Ns Q MN Ms_env Ns_env MsNs IH MMs. inversion MsNs. constructor. inversion MsNs. assert (IHrest: forall L L' R R', subterm L M \/ (L = M /\ In R Ms) -> L ~(Q) L' -> R ~(Q) R' -> L >> R -> env L' = env R' -> L' >> R'). intros. apply IH with L R; trivial. destruct H4; auto. right; destruct H4; split; auto with datatypes. inversion MMs. constructor 2. apply IH with M a; auto with datatypes. rewrite <- (Ns_env y); trivial. rewrite <- H2; auto with datatypes. apply IHMs with Q; trivial. intros; apply Ms_env; auto with datatypes. intros; apply Ns_env; rewrite <- H2; auto with datatypes. constructor 3. destruct H7 as [M' M'arg M'ord]. destruct (conv_arg M' MN) as [W [WN M'W]]; trivial. exists W; auto. destruct M'ord. constructor 1. apply IH with M1 N1; auto with datatypes. left; apply arg_subterm; trivial. rewrite (appUnit_env W N); auto with terms. sym; apply Ns_env; rewrite <- H2; auto with datatypes. replace W with y. constructor 2. apply term_eq. rewrite (appUnit_env W N); auto with terms. apply Ns_env; rewrite <- H2; auto with datatypes. apply conv_term_unique with (term M1) Q; fo. apply IHMs with Q; auto with datatypes. intros; apply Ns_env; rewrite <- H2; auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)