∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I},
  π.IsPartition →
    ∀ {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
      (∀ J ∈ π, (πi J).IsPartition) → (π.biUnionPrepartition πi).IsPartition