proposition: Lemma horpo_neutral_comp_step : forall M, algebraic M -> isNeutral M -> (CompH M <-> (forall N, M >> N -> CompH N)).
proof: Proof. intros M Mneutral; unfold CompH. apply neutral_comp_step; eauto with horpo. Qed.
imports: CoLoR(RelExtras ListExtras Computability Horpo) Coq(Setoid Morphisms)