proposition: Theorem PRF_DRBG_f_bad_2_compMap_equiv : forall n, comp_spec eq (PRF_DRBG_f_bad_2 n) (compMap (Bvector_EqDec eta) (fun _ : nat => { 0 , 1 }^eta) (forNats n)).
proof: Proof. induction n; intuition; simpl in *. fcf_reflexivity. fcf_skip. fcf_skip. apply IHn. subst. fcf_reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF