proposition: Lemma DN_apply {T: Type}: DN T -> forall P, Stable P -> (T -> P) -> P.
proof: Proof. firstorder. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.Classes.Morphisms