no goals
α✝ : Type ?u.165055
β : Type ?u.165058
γ : Type ?u.165061
ι : Sort ?u.165064
ι' : Sort ?u.165067
ι₂ : Sort ?u.165070
κ : ι → Sort ?u.165075
κ₁ : ι → Sort ?u.165080
κ₂ : ι → Sort ?u.165085
κ' : ι' → Sort ?u.165090
α : Type u_1
⊢ (⋃ (x : α), {x}) = univ
simp [Set.ext_iff]