proposition: Theorem PRF_DRBG_f_bad_2_equiv : forall n v, comp_spec (fun x1 x2 => x1 = v :: (map injD x2)) (PRF_DRBG_f_bad v (S n)) (PRF_DRBG_f_bad_2 n).
proof: Proof. induction n; intuition; simpl in *. fcf_irr_l. fcf_simp. fcf_spec_ret. fcf_skip. fcf_skip. fcf_spec_ret. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF