proposition: Lemma DN_lunit: ext_eq -> forall A B (a: A) (f: A -> DN B), DN_bind (DN_return a) _ f = f a.
proof: Proof. firstorder. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.Classes.Morphisms