proposition: Theorem PRF_DRBG_f_G2_compMap_spec : forall n v, comp_spec (fun x1 x2 => fst x1 = x2) ((PRF_DRBG_f_G2 v n) unit unit_EqDec (fun (_ : unit) (_ : D) => x <-$ { 0 , 1 }^eta; ret (x, tt)) tt) (compMap (Bvector_EqDec eta) (fun _ : nat => { 0 , 1 }^eta) (forNats n)).
proof: Proof. induction n; intuition; simpl in *. fcf_simp. fcf_spec_ret. fcf_inline_first. fcf_skip. fcf_skip. fcf_spec_ret. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF