proposition: Theorem G0_G1_equiv : | Pr[G0] - Pr[G1] | <= PRF_Advantage ({0, 1}^c) ({0, 1}^c) h _ _ PRF_h_A.
proof: Proof. rewrite G0_G1_1_equiv. rewrite <- G1_2_G1_equiv. eapply G1_1_2_close. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv