{R : Type u_1} →
  [inst : CommRing R] →
    {motive : IsDedekindDomain.HeightOneSpectrum R → Sort u} →
      (t : IsDedekindDomain.HeightOneSpectrum R) →
        ((asIdeal : Ideal R) →
            (isPrime : asIdeal.IsPrime) →
              (ne_bot : asIdeal ≠ ⊥) → motive { asIdeal := asIdeal, isPrime := isPrime, ne_bot := ne_bot }) →
          motive t