proposition: Theorem G2_3_4_equiv : Pr[x <-$ G2_3; ret fst x] == Pr[x <-$ G2_4; ret fst x].
proof: Proof. unfold G2_3, G2_4. do 4 (inline_first; comp_skip; comp_simp). inline_first. eapply comp_spec_impl_eq. eapply comp_spec_seq; eauto with inhabited. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = fst b)); intuition. destruct x3; simpl in *; subst. unfold RF_Encrypt. clear H2. 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