no goals
α : Type u_2
β : Type u_1
γ : Type ?u.113795
ι : Sort ?u.113798
ι' : Sort ?u.113801
ι₂ : Sort ?u.113804
κ : ι → Sort ?u.113809
κ₁ : ι → Sort ?u.113814
κ₂ : ι → Sort ?u.113819
κ' : ι' → Sort ?u.113824
a b : α
s : α → Set β
⊢ (⋃ (x : α) (_ : x ∈ {a, b}), s x) = s a ∪ s b
simp