proposition: Lemma comp_manysteps_comp : forall M N, Computable M -> M -R*-> N -> Computable N.
proof: Proof. intros M N Mcomp M_rew_N. induction M_rew_N. apply comp_step_comp with x; trivial. auto. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)