∀ {α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [inst : DecidablePred p] (f : (i : ι) → p i → Set α)
  (g : (i : ι) → ¬p i → Set α),
  (⋂ i, if h : p i then f i h else g i h) = (⋂ i, ⋂ (h : p i), f i h) ∩ ⋂ i, ⋂ (h : ¬p i), g i h