proposition: Lemma conv_arg : forall M Marg N Q, M ~(Q) N -> isArg Marg M -> exists Narg, isArg Narg N /\ Marg ~(Q) Narg.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall Marg N Q, M ~(Q) N -> isArg Marg M -> exists Narg, isArg Narg N /\ Marg ~(Q) Narg). apply subterm_wf. clear M; intros M IH Marg N Q MN MargM. unfold isArg in MargM. destruct (isApp_dec M) as [Mapp | Mnapp]. rewrite (appArgs_app M Mapp) in MargM. set (Napp := proj1 (isApp_morph (conv_by MN)) Mapp). destruct (in_app_or MargM). set (Msub := appBodyL_subterm M Mapp). destruct (IH (appBodyL Mapp) Msub Marg (appBodyL Napp) Q) as [Narg [NargN MNargs]]; trivial. apply app_conv_app_left_aux; trivial. exists Narg; split; trivial. apply appArg_left with Napp; trivial. inversion H; try_solve. exists (appBodyR Napp); split. apply appArg_right with Napp; trivial. rewrite <- H0. apply app_conv_app_right_aux; trivial. rewrite appArgs_notApp in MargM; trivial. inversion MargM. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)