{α : Type u} →
  {motive : PseudoMetricSpace α → Sort u_1} →
    (t : PseudoMetricSpace α) →
      ([toDist : Dist α] →
          (dist_self : ∀ (x : α), dist x x = 0) →
            (dist_comm : ∀ (x y : α), dist x y = dist y x) →
              (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) →
                (edist : α → α → ENNReal) →
                  (edist_dist : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) →
                    (toUniformSpace : UniformSpace α) →
                      (uniformity_dist : uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}) →
                        (toBornology : Bornology α) →
                          (cobounded_sets :
                              (Bornology.cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}) →
                            motive
                              { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm,
                                dist_triangle := dist_triangle, edist := edist, edist_dist := edist_dist,
                                toUniformSpace := toUniformSpace, uniformity_dist := uniformity_dist,
                                toBornology := toBornology, cobounded_sets := cobounded_sets }) →
        motive t