proposition: Theorem PRF_DRBG_G3_1_2_eq : Pr[PRF_DRBG_G3_1] == Pr[x <-$ PRF_DRBG_G3_2; ret (fst x)].
proof: Proof. unfold PRF_DRBG_G3_1, PRF_DRBG_G3_2. simpl. fcf_inline_first. fcf_skip. fcf_simp. fcf_inline_first. fcf_skip. fcf_simp. simpl. fcf_reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF