proposition: Theorem PRF_DRBG_G3_3_G4_eq : Pr[ x <-$ PRF_DRBG_G3_3; ret (fst x) ] == Pr[ PRF_DRBG_G4 ].
proof: Proof. unfold PRF_DRBG_G3_3, PRF_DRBG_G4. simpl. fcf_inline_first. fcf_to_prhl_eq. fcf_skip. eapply (fcf_oracle_eq (fun x1 x2 => True)); intuition. fcf_skip. fcf_spec_ret. simpl in H1. intuition; subst. fcf_simp. fcf_inline_first. simpl. fcf_skip. simpl; fcf_simp. fcf_reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF