proposition: Lemma appArgs_conv : forall M N Q, M ~(Q) N -> conv_list (appArgs M) (appArgs N) Q.
proof: Proof. intros. set (w := appUnits_conv H). inversion w. set (p := appUnits_not_nil M); try_solve. unfold appArgs. rewrite <- H0; rewrite <- H1; simpl; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)