proposition: Theorem Rnd_NG_unique : forall (F : R -> Prop) (P : R -> R -> Prop), Rnd_NG_pt_unique_prop F P -> forall rnd1 rnd2 : R -> R, Rnd_NG F P rnd1 -> Rnd_NG F P rnd2 -> forall x, rnd1 x = rnd2 x.
proof: Proof. intros F P HP rnd1 rnd2 H1 H2 x. now apply Rnd_NG_pt_unique with F P x. Qed.
imports: Coq(Reals) Raux Defs