proposition: Lemma headFunS_dec : forall M, {isFunS (appHead M)} + {~isFunS (appHead M)}.
proof: Proof. destruct M as [E Pt A M]; induction M. fo. fo. fo. rewrite (appHead_app (buildT (TApp M1 M2)) I). destruct IHM1; fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)