proposition: Theorem PRF_A'_admissible : admissible_oc cost _ _ _ (fun n => PRF_A' (A1 n) (@A2 n)).
proof: Proof. unfold admissible_oc. intuition. eapply PRF_A'_wf. eapply PRF_A'_poly_time. eapply PRF_A'_poly_queries. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime Asymptotic