∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}
  (motive : (∃ S, S.Countable ∧ (∀ s ∈ S, IsOpen s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y) → Prop)
  (x : ∃ S, S.Countable ∧ (∀ s ∈ S, IsOpen s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  (∀ (S : Set (Set X)) (hSc : S.Countable) (hSo : ∀ s ∈ S, IsOpen s)
      (hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y), motive ⋯) →
    motive x