proposition: Lemma algebraic_arrowType : forall M, algebraic M -> isArrowType (type M) -> ~isFunApp M.
proof: Proof. intros. assert (forall T, isBaseType T -> isArrowType T -> False). destruct T; try_solve. unfold isFunApp. inversion H; try_solve; fo; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)