{α : Type u} →
  [inst : TopologicalSpace α] →
    {motive : ConnectedSpace α → Sort u_1} →
      ([toPreconnectedSpace : PreconnectedSpace α] → (toNonempty : Nonempty α) → motive ⋯) →
        (t : ConnectedSpace α) → motive t