no goals
α : Type u_1
β : Type ?u.88687
γ : Type ?u.88690
ι : Sort u_2
ι' : Sort u_3
ι₂ : Sort ?u.88699
κ : ι → Sort ?u.88704
κ₁ : ι → Sort ?u.88709
κ₂ : ι → Sort ?u.88714
κ' : ι' → Sort ?u.88719
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 [iUnion_and, @iUnion_comm _ ι']