proposition: Lemma CompCaseBasic : forall M, Computable M -> isBaseType M.(type) -> AccR M.
proof: Proof. intros M Mcomp Mbase. destruct (CompCase M Mcomp) as [[_ [Macc _]] | [Marr _]]. trivial. destruct (type M); contr. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)