no goals
α : Type u_1
β : Type ?u.91348
γ : Type ?u.91351
ι : Sort u_2
ι' : Sort u_3
ι₂ : Sort ?u.91360
κ : ι → Sort ?u.91365
κ₁ : ι → Sort ?u.91370
κ₂ : ι → Sort ?u.91375
κ' : ι' → Sort ?u.91380
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ (⋂ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h) = ⋂ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y (_ : p x ∧ q x y)
simp only [iInter_and, @iInter_comm _ ι']