proposition: Theorem PRF_DRBG_G1_G2_equiv : Pr[ PRF_DRBG_G1 ] == Pr[ PRF_DRBG_G2 ].
proof: Proof. rewrite PRF_DRBG_G1_1_equiv. unfold PRF_DRBG_G1_1, PRF_DRBG_G2. unfold PRF_A. simpl. fcf_skip. fcf_inline_first. fcf_to_prhl_eq. fcf_with PRF_DRBG_f_G1_1_G2_equiv fcf_skip. fcf_simp. simpl. fcf_inline_first. fcf_ident_expand_l. fcf_skip. fcf_simp. fcf_reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF