proposition: Lemma appHead_app_aux : forall M (Mapp: isApp M), head (appUnits M) = head (appUnits (appBodyL Mapp)).
proof: Proof. intro M; term_inv M. rewrite (appUnits_app Tr I). simpl. rewrite head_app. trivial. apply appUnits_not_nil. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)