proposition: Lemma isFunApp_dec : forall M, {isFunApp M} + {~isFunApp M}.
proof: Proof. destruct M as [E Pt A M]; destruct M. fo. fo. fo. destruct (headFunS_dec (buildT (TApp M1 M2))) as [headF | headNF]; fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)