proposition: Lemma comp_imp_acc : forall M, Computable M -> AccR M.
proof: Proof. intros M MC. destruct (comp_prop (type M)) as [P1 P2]. apply P1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)