proposition: Lemma funApp : forall M f, term (appHead M) = ^f -> isApp M -> isFunApp M.
proof: Proof. unfold isFunApp; intros M f Mhead Mapp. term_inv (appHead M). Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)