∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι),
  BoxIntegral.Prepartition.splitCenter I =
    { boxes := Finset.map I.splitCenterBoxEmb Finset.univ, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }