∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)),
  ∃ x,
    (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≠ 0 ∧ (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≠ 1