proposition: Lemma horpo_comp_manysteps_comp M N : CompH M -> M >>* N -> CompH N.
proof: Proof. intros Mcomp M_N. unfold CompH; apply comp_manysteps_comp with M; eauto with horpo. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)