proposition: Lemma CompArrow : forall M, algebraic M -> isArrowType (type M) -> (forall N (Napp: isApp N), (appBodyL Napp) ~ M -> algebraic (appBodyR Napp) -> Computable (appBodyR Napp) -> Computable N) -> Computable M.
proof: Proof. intros [E Pt [?|A1 A2] Typ];try_solve; intros. hnf; intros; split; trivial. split; trivial. intros; unfold Computable in H1. rewrite <- typeL. apply H1 with Papp; trivial. rewrite (@app_typeR P A1 A2 Papp); trivial. rewrite (terms_conv_eq_type PL); trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)