proposition: Theorem G2_2_3_badness_same : Pr[x <-$ G2_2; ret (snd x)] == Pr[x <-$ G2_3; ret (snd x)].
proof: Proof. pose proof RF_Encrypt_wf. unfold G2_2, G2_3. do 3 (inline_first; comp_skip; comp_simp). comp_inline_l. comp_irr_l; wftac. eapply randomFunc_wf; wftac. comp_inline_r. comp_irr_r; wftac. comp_simp. comp_inline_l. comp_irr_l; wftac. eapply oc_comp_wf; intuition. comp_inline_r. comp_irr_r; wftac. eapply oc_comp_wf; intuition. comp_simp. simpl. intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime