no goals
α : Type u_1
β : Type u_2
γ : Type ?u.100478
ι : Sort ?u.100481
ι' : Sort ?u.100484
ι₂ : Sort ?u.100487
κ : ι → Sort ?u.100492
κ₁ : ι → Sort ?u.100497
κ₂ : ι → Sort ?u.100502
κ' : ι' → Sort ?u.100507
a : α
s : Set α
t : α → Set β
⊢ (⋂ (x : α) (_ : x ∈ insert a s), t x) = t a ∩ ⋂ (x : α) (_ : x ∈ s), t x
simp