proposition: Theorem PRF_DRBG_G4_DRBG_equiv : Pr[PRF_DRBG_G4] == Pr[DRBG_G1 RndOut A].
proof: Proof. unfold PRF_DRBG_G4, DRBG_G1, RndOut, PRF_A. simpl. fcf_inline_first. fcf_to_prhl_eq. fcf_with PRF_DRBG_f_G2_compMap_spec fcf_skip. simpl. fcf_inline_first. fcf_ident_expand_r. fcf_skip. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF