proposition: Theorem satisfies_any_eq : forall F1 F2 : R -> Prop, ( forall x, F1 x <-> F2 x ) -> satisfies_any F1 -> satisfies_any F2.
proof: Proof. intros F1 F2 Heq (Hzero, Hsym, Hrnd). split. now apply -> Heq. intros x Hx. apply -> Heq. apply Hsym. now apply <- Heq. intros x. destruct (Hrnd x) as (f, (H1, (H2, H3))). exists f. split. now apply -> Heq. split. exact H2. intros g Hg Hgx. apply H3. now apply <- Heq. exact Hgx. Qed.
imports: Coq(Reals) Raux Defs