proposition: Lemma conv_arg_rev : forall M N Narg Q, M ~(Q) N -> isArg Narg N -> exists Marg, isArg Marg M /\ Marg ~(Q) Narg.
proof: Proof. intros. set (NM := terms_conv_sym_aux H). destruct (conv_arg Narg NM) as [Marg [MargM NMarg]]; trivial. exists Marg; split; trivial. rewrite <- (envSubst_transp_twice Q). apply terms_conv_sym_aux; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)