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