no goals
α : Type u_1
β : Type u_2
γ : Type ?u.111642
ι : Sort ?u.111645
ι' : Sort ?u.111648
ι₂ : Sort ?u.111651
κ : ι → Sort ?u.111656
κ₁ : ι → Sort ?u.111661
κ₂ : ι → Sort ?u.111666
κ' : ι' → Sort ?u.111671
a : α
s : Set α
t : α → Set β
⊢ (⋃ (x : α) (_ : x ∈ insert a s), t x) = t a ∪ ⋃ (x : α) (_ : x ∈ s), t x
simp