proposition: Lemma CompCaseArrow : forall M, Computable M -> isArrowType M.(type) -> forall N (Napp: isApp N), algebraic (appBodyR Napp) -> Computable (appBodyR Napp) -> (appBodyL Napp) ~ M -> Computable N.
proof: Proof. intros M Mcomp Marr. destruct (CompCase M Mcomp) as [[Mbase _] | [_ [_ H]]]. destruct (type M); contr. trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)