proposition: Lemma notFunApp_left: forall M (Mapp: isApp M), ~isFunApp (appBodyL Mapp) -> ~isFunApp M.
proof: Proof. intros. intro. absurd (isFunApp (appBodyL Mapp)); trivial. apply isFunApp_left; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)