proposition: Lemma app_units_app : forall M (Mapp: isApp M), appUnits M = appHead M :: nil ++ appArgs M.
proof: Proof. destruct M as [E Pt T M]; induction M; try_solve. simpl. rewrite (appUnits_app (buildT (TApp M1 M2)) I). rewrite (appArgs_app (buildT (TApp M1 M2)) I). rewrite (appHead_app (buildT (TApp M1 M2)) I). simpl. destruct (isApp_dec (buildT M1)). rewrite IHM1; trivial. rewrite (appUnits_notApp (buildT M1) n). rewrite (appArgs_notApp (buildT M1) n). rewrite (appHead_notApp (buildT M1) n). trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)