proposition: Theorem hF_PRF : PRF_Advantage ({0, 1}^(c + k)) ({0, 1}^c) hF _ _ A <= PRF_Advantage ({0, 1}^c) ({0, 1}^c) h _ _ PRF_h_A + Adv_WCR _ _ F (Rnd k) au_F_A.
proof: Proof. unfold PRF_Advantage. rewrite G0_equiv. eapply ratDistance_le_trans. eapply G0_G1_equiv. rewrite <- G2_equiv. eapply G1_G2_equiv. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv