proposition: Theorem TwoWorlds_equiv : negligible (fun eta => (| Pr[f eta false] - Pr[f eta true] |)) <-> negligible (fun eta => | Pr[StandardDef_G eta] - 1 / 2 |).
proof: Proof. intuition. eapply TwoWorlds_equiv_f; intuition. eapply TwoWorlds_equiv_b; intuition. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic