no goals
α : Type u_1
β : Type ?u.108307
γ : Type ?u.108310
ι : Sort ?u.108313
ι' : Sort ?u.108316
ι₂ : Sort ?u.108319
κ : ι → Sort ?u.108324
κ₁ : ι → Sort ?u.108329
κ₂ : ι → Sort ?u.108334
κ' : ι' → Sort ?u.108339
s : Set α
⊢ ∀ (x : α), (x ∈ ⋃ (x : α) (_ : x ∈ s), {x}) ↔ x ∈ s
simp