proposition: Lemma CompBasic : forall M, isBaseType M.(type) -> algebraic M -> AccR M -> Computable M.
proof: Proof. intro M; term_type_inv M; split; trivial. split; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)