proposition: Theorem PRF_DRBG_f_G1_1_eq_ret : forall k n v, comp_spec eq (PRF_DRBG_f_G1_1 v n k) (ret (PRF_DRBG_f v n k)).
proof: Proof. induction n; intuition; simpl in *. fcf_reflexivity. fcf_simp. fcf_transitivity. fcf_skip_eq. fcf_reflexivity. fcf_simp. fcf_reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF