∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ),
  BoxIntegral.Prepartition.splitMany I (insert p s) =
    BoxIntegral.Prepartition.splitMany I s ⊓ BoxIntegral.Prepartition.split I p.1 p.2