proposition: Theorem G2_2_bad_small : Pr[x <-$ G2_2; ret snd x] <= q1 / (2 ^ eta).
proof: Proof. pose proof RF_Encrypt_wf. rewrite G2_2_bad_equiv. unfold G2_2_bad. comp_irr_l. eapply oc_comp_wf; intuition. comp_simp. assert (length l <= q1)%nat. eapply qam_count; eauto. eapply RF_Encrypt_length_incr. simpl; intuition. eapply RndInList_prob. rewrite split_length_l. trivial. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime