proposition: Theorem Rnd_DN_unique : forall F : R -> Prop, forall rnd1 rnd2 : R -> R, Rnd_DN F rnd1 -> Rnd_DN F rnd2 -> forall x, rnd1 x = rnd2 x.
proof: Proof. intros F rnd1 rnd2 H1 H2 x. now eapply Rnd_DN_pt_unique. Qed.
imports: Coq(Reals) Raux Defs