proposition: Lemma DN_runit: ext_eq -> forall A (x: DN A), DN_bind x _ DN_return = x.
proof: Proof. intros. cut (forall y y', y = y' -> x y = x y'). firstorder. congruence. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.Classes.Morphisms