proposition: Theorem G2_5_G3_equiv : Pr[x <-$ G2_5; ret fst x] == Pr[G3].
proof: Proof. unfold G2_5, G3. intuition. inline_first. comp_at comp_inline leftc 1%nat. comp_swap_l. comp_skip. comp_simp. comp_swap_r. comp_skip. comp_inline_l. comp_skip. inline_first; comp_skip. inline_first. eapply comp_spec_impl_eq. eapply comp_spec_seq; eauto with inhabited. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => fst a = b)); intuition. simpl in *; subst. unfold RF_Encrypt. comp_skip. comp_skip. eapply comp_spec_ret; simpl in *; intuition. intuition. simpl in *; subst. prog_simp. eapply comp_spec_ret; simpl in *; intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime