proposition: Theorem PRF_DRBG_G3_bad_equiv : Pr[x <-$ PRF_DRBG_G3_3; ret (snd x)] == Pr[PRF_DRBG_G3_bad_1].
proof: Proof. unfold PRF_DRBG_G3_3, PRF_DRBG_G3_bad_1. simpl. fcf_inline_first. fcf_to_prhl_eq. fcf_skip. apply PRF_DRBG_f_bad_spec. simpl in H1. fcf_inline_first. fcf_irr_l. fcf_simp. simpl. fcf_spec_ret. apply Permutation_hasDups. trivial. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF