∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ)
  (h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I),
  J ∈ { toPrepartition := π, tag := f, tag_mem_Icc := h } ↔ J ∈ π