no goals
α : Type u_1
β : Type ?u.166144
γ : Type ?u.166147
ι : Sort ?u.166150
ι' : Sort ?u.166153
ι₂ : Sort ?u.166156
κ : ι → Sort ?u.166161
κ₁ : ι → Sort ?u.166166
κ₂ : ι → Sort ?u.166171
κ' : ι' → Sort ?u.166176
s : Set α
⊢ (⋃ (i : ↑s), {↑i}) = s
simp