proposition: Theorem G2_3_4_close : | Pr[x <-$ G2_3; ret fst x] - Pr[x <-$ G2_4; ret fst x] | <= Adv_WCR _ _ F (Rnd k) au_F_A.
proof: Proof. eapply leRat_trans. eapply fundamental_lemma_h. eapply G2_3_4_bad_eq . eapply G2_3_4_eq_until_bad. rewrite G2_3_bad_equiv. rewrite G2_3_bad_small. intuition. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv