∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {p p_1 : Ideal R} (e_p : p = p_1) (hp : Prime p),
  IsDedekindDomain.HeightOneSpectrum.ofPrime hp = IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯