∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (I : FractionalIdeal (nonZeroDivisors R) K),
  ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, FractionalIdeal.count K v I = 0