∀ {α : Type u_1} {p₁ : Set α → Prop} {t₁ : Set α}
  (motive : (∃ S, S.Countable ∧ (∀ s ∈ S, p₁ s) ∧ ∀ x ∈ t₁, ∀ y ∈ t₁, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y) → Prop)
  (x : ∃ S, S.Countable ∧ (∀ s ∈ S, p₁ s) ∧ ∀ x ∈ t₁, ∀ y ∈ t₁, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  (∀ (S : Set (Set α)) (hSc : S.Countable) (hSp : ∀ s ∈ S, p₁ s)
      (hSt : ∀ x ∈ t₁, ∀ y ∈ t₁, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y), motive ⋯) →
    motive x