proposition: Lemma notFunApp_left_eq : forall M (Mapp: isApp M) N (Napp: isApp N), ~isFunApp M -> appBodyL Mapp = appBodyL Napp -> ~isFunApp N.
proof: Proof. intro M; term_inv M. intros _ N; term_inv N. intros. apply notFunApp_left with I. simpl; rewrite <- H0. change (buildT T1) with (appBodyL (M:=buildT (TApp T1 T2)) I). apply notFunApp_left_inv; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)