∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A} [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B] [inst_4 : IsDomain A] [inst_5 : Module.IsTorsionFree A B]
  (hp : p ≠ 0),
  IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp = IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp