proposition: Theorem G2_PRF_A'_equiv : Pr[[b, _] <-$2 PRF_A _ _ PRFE_RandomFunc nil; ret b] == Pr[[b, _] <-$2 PRF_A' _ _ PRFE_RandomFunc nil; ret b].
proof: Proof. intuition. comp_skip. eapply PRF_A'_equiv. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime