proposition: Lemma appArg_conv_appArg : forall M M' N Q, M ~(Q) N -> isArg M' M -> exists N', isArg N' N /\ M' ~(Q) N'.
proof: Proof. intros. destruct (list_In_nth (appArgs M) M' H0) as [p Mp]. set (MNargs := appArgs_conv H). destruct (list_sim_nth p MNargs Mp) as [N' [Np M'N']]. exists N'; split; trivial. unfold isArg; apply nth_some_in with p; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)