proposition: Theorem G1_G2_close : |Pr[G1] - Pr[G2]| == PRF_Advantage ({0, 1}^eta) ({0, 1}^eta) f _ _ PRF_A'.
proof: Proof. rewrite G1_PRF_A_equiv. rewrite G1_PRF_A'_equiv. rewrite G2_PRF_A_equiv. rewrite G2_PRF_A'_equiv. reflexivity. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime