proposition: Theorem PRF_NAI_Advantage_eq_Hybrid: PRF_NAI_Advantage == ListHybrid_Advantage (fun lsD => k <-$ RndKey; ret (map (f k) lsD)) (fun lsD => [lsR, _] <-$2 oracleMap _ _ RndR_func nil lsD; ret lsR) _ A1 A2.
proof: Proof. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid