∀ {α : Type u_1} {ι : Type u_2} (p1 : Finset ι) (f1 : ι → Set α) (p2 : Finset ι) (f2 : ι → Set α),
  ∀ n ∈ p1,
    n ∈ p2 → f1 n ∩ f2 n = ∅ → (fun n => (if n ∈ p1 then f1 n else Set.univ) ∩ if n ∈ p2 then f2 n else Set.univ) n ⊆ ∅