proposition: Theorem PRF_DRBG_G1_1_equiv : Pr[PRF_DRBG_G1] == Pr[PRF_DRBG_G1_1].
proof: Proof. unfold PRF_DRBG_G1, PRF_DRBG_G1_1. fcf_skip. fcf_to_prhl_eq. fcf_symmetry. fcf_transitivity. fcf_with PRF_DRBG_f_G1_1_eq_ret fcf_skip_eq. fcf_reflexivity. fcf_simp. fcf_reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF