proposition: Lemma appArgs_app : forall M (Mapp: isApp M), appArgs M = appArgs (appBodyL Mapp) ++ (appBodyR Mapp)::nil.
proof: Proof. intros M Mapp; unfold appArgs. rewrite (appUnits_app M Mapp). sym; auto with terms datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)