∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {ι : Sort u_4} [Countable ι] {p : α → ι → Prop},
  (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) = ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i