proposition: Theorem Rnd_NA_unique : forall (F : R -> Prop), F 0 -> forall rnd1 rnd2 : R -> R, Rnd_NA F rnd1 -> Rnd_NA F rnd2 -> forall x, rnd1 x = rnd2 x.
proof: Proof. intros F HF rnd1 rnd2 H1 H2 x. now apply Rnd_NA_pt_unique with F x. Qed.
imports: Coq(Reals) Raux Defs