proposition: Theorem G2_2_3_close : forall z, | evalDist (x <-$ G2_2; ret fst x) z - evalDist (x <-$ G2_3; ret fst x) z | <= q1 / (2 ^ eta).
proof: Proof. intuition. eapply leRat_trans. eapply fundamental_lemma_h. eapply G2_2_3_badness_same. eapply G2_2_3_eq_until_bad. eapply G2_2_bad_small. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime