{X : Type u_4} →
  [inst : TopologicalSpace X] →
    {motive : StronglyLocallyContractibleSpace X → Sort u} →
      (t : StronglyLocallyContractibleSpace X) →
        ((contractible_basis : ∀ (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ ContractibleSpace ↑s) id) →
            motive ⋯) →
          motive t