proposition: Theorem PRF_DRBG_f_G1_1_G2_equiv : forall k n v, comp_spec (fun x1 x2 => x1 = fst x2) (PRF_DRBG_f_G1_1 v n k) ((PRF_DRBG_f_G2 v n) unit unit_EqDec (f_oracle f (Bvector_EqDec eta) k) tt).
proof: Proof. induction n; intuition; simpl in *. fcf_simp. fcf_spec_ret. fcf_skip. unfold f_oracle. eapply (comp_spec_ret _ _ (fun x1 x2 => x1 = fst x2)). trivial. simpl in *. intuition; subst. fcf_skip. fcf_simp. fcf_spec_ret. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF