proposition: Lemma comp_algebraic : forall M, Computable M -> algebraic M.
proof: Proof. intros. unfold Computable in H; destruct (type M); simpl in H; destruct H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)