proposition: Lemma funApp_head : forall M, isFunApp M -> { f: FunctionSymbol | term (appHead M) = ^f }.
proof: Proof. unfold isFunApp; intros M MfunApp. term_inv (appHead M). exists f; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)