proposition: Lemma funAbs_notFunApp : forall M, isAbs (appHead M) -> ~isFunApp M.
proof: Proof. unfold isFunApp; intros. term_inv M. intro Tr_fa. term_inv (appHead Tr). Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)