proposition: Theorem G2_2_bad_equiv : Pr[x <-$ G2_2; ret snd x] == Pr[G2_2_bad].
proof: Proof. pose proof RF_Encrypt_wf. rewrite G2_2_3_badness_same. unfold G2_3, G2_2_bad. inline_first. comp_at comp_inline leftc 1%nat. comp_swap_l. comp_skip. comp_simp. comp_skip. do 3 (comp_inline_l; comp_irr_l; wftac). eapply oc_comp_wf; intuition. comp_simp. eapply evalDist_ret_eq; simpl. case_eq (arrayLookup (Bvector_EqDec eta) l x); intuition; destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x (fst (split l))); intuition. exfalso. eauto using arrayLookup_In_split. exfalso. eapply (@arrayLookup_not_In_split _ _ (Bvector_EqDec eta)). eauto. trivial. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime