proposition: Theorem G2_1_equiv : Pr[G2] == Pr[G2_1].
proof: Proof. unfold G2, G2_1. do 2 (comp_swap_r; comp_skip; comp_simp). unfold RF_Encrypt. do 2(inline_first; comp_skip; comp_simp). intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime