proposition: Lemma algebraic_app_notFunApp : forall M (Mapp: isApp M), algebraic (appBodyL Mapp) -> algebraic (appBodyR Mapp) -> ~isFunApp M.
proof: Proof. intros; intro i. assert (~isApp (appBodyL Mapp) -> isFunS (appBodyL Mapp)). intro Lnapp. unfold isFunApp in i. rewrite (appHead_app M Mapp) in i; simpl. rewrite (appHead_notApp (appBodyL Mapp)) in i; trivial. inversion H; try solve [term_inv M | term_inv (appBodyL Mapp)]. absurd (isFunApp (appBodyL Mapp)); trivial. unfold isFunApp in * . rewrite (appHead_app M Mapp) in i; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)