proposition: Lemma notFunApp_left_inv : forall M (Mapp: isApp M), ~isFunApp M -> ~isFunApp (appBodyL Mapp).
proof: Proof. unfold isFunApp; intros; intro MLfa. absurd (isFunApp M); trivial. term_inv M. unfold isFunApp; rewrite (appHead_app Tr I); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)