∀ {X : Type u_1} [inst : LinearOrder X] {s : Set X}
  (motive :
    (∃ S, S.Countable ∧ (∀ s ∈ S, s ∈ Set.range Set.Ioi) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y) → Prop)
  (x : ∃ S, S.Countable ∧ (∀ s ∈ S, s ∈ Set.range Set.Ioi) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  (∀ (t : Set (Set X)) (htc : t.Countable) (ht_sub : ∀ s ∈ t, s ∈ Set.range Set.Ioi)
      (ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y), motive ⋯) →
    motive x