proposition: Lemma horpo_conv_comp : forall M N M' N' Q, M ~(Q) M' -> N ~(Q) N' -> M >> N -> env M' = env N' -> M' >> N'.
proof: Proof. intros M N. assert (Res: forall P M' N' Q, (fst P) ~(Q) M' -> (snd P) ~(Q) N' -> fst P >> snd P -> env M' = env N' -> M' >> N'). intro P. apply well_founded_ind with (R := LexProd_Lt) (P := fun P => forall M' N' Q, (fst P) ~(Q) M' -> (snd P) ~(Q) N' -> fst P >> snd P -> env M' = env N' -> M' >> N'). 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 M' N' Q MM' NN' MN M'N'. destruct P as [M N]; simpl in * . apply horpo_conv_comp_aux with M N Q; trivial. intros. apply IH with (L, R) Q0; trivial. destruct H. constructor; exact H. destruct H; rewrite H. constructor 2; trivial. auto with sets. intros. apply Res with (M, N) Q; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)