fact: Definition PRF_NA := forall (State : DataTypeFamily) A1 A2, admissible_A1 _ A1 -> admissible_A2 State _ _ A2 -> negligible (fun n => PRF_NA_Advantage (RndKey n) (RndR n) (@f n) _ _ (A1 n) (@A2 n)).
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid FCF.Asymptotic FCF.Admissibility