proposition: Lemma neutral_comp_step : forall M, algebraic M -> isNeutral M -> (Computable M <-> (forall N, M -R-> N -> Computable N)).
proof: Proof. intros M Mneutral. destruct (comp_prop (type M)) as [P1 P2]. split. intros Mcomp N MN. apply comp_step_comp with M; trivial. intros MNcomp. apply P2; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)