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