proposition: Lemma CompCase : forall M, Computable M -> { isBaseType M.(type) /\ AccR M /\ algebraic M } + { isArrowType M.(type) /\ algebraic M /\ forall N (Napp: isApp N), algebraic (appBodyR Napp) -> Computable (appBodyR Napp) -> (appBodyL Napp) ~ M -> Computable N }.
proof: Proof. intro M. destruct M as [E Pt A0 Typ]. revert Typ. destruct A0; intro Typ; try_solve; intro; unfold Computable in H; simpl in H; inversion H. inversion H1; left; do 2 split; trivial. right; do 2 split; trivial. intros N Napp Nnorm NR NL. unfold Computable. term_inv N. set (w := terms_conv_eq_type NL). inversion w. inversion H1. apply H5 with Napp; trivial. unfold Computable in NR. rewrite <- H3; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)