{X : Type u_3} →
  [inst : TopologicalSpace X] →
    {motive : LocallyCompactSpace X → Sort u} →
      (t : LocallyCompactSpace X) →
        ((local_compact_nhds : ∀ (x : X), ∀ n ∈ nhds x, ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s) → motive ⋯) → motive t