proposition: Lemma algebraic_funApp_datatype : forall M, algebraic M -> isFunApp M -> isBaseType (type M).
proof: Proof. unfold isFunApp; intros. inversion H; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)