proposition: Lemma appHead_app : forall M (Mapp: isApp M), appHead M = appHead (appBodyL Mapp).
proof: Proof. intro M; term_inv M. unfold appHead. destruct (head_notNil (appUnits_not_nil Tr)). destruct (head_notNil (appUnits_not_nil (buildT T1))). simpl. assert (head (appUnits Tr) = head (appUnits (buildT T1))). change (buildT T1) with (@appBodyL Tr I). apply appHead_app_aux. congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)