fact: Fixpoint PRF_DRBG_f_G2 (v : D)(n : nat) := match n with | O => $ ret nil | S n' => r <--$ (OC_Query _ v); ls' <--$ (PRF_DRBG_f_G2 (injD r) n'); $ ret (r :: ls') end.
imports: FCF HasDups RndInList CompFold Permutation PRF