∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} (x : BoxIntegral.Box ι),
  ↑x ≤ I₀ → ∀ (x_2 : BoxIntegral.Prepartition x), x_2.IsPartition → ∑ _x ∈ x_2.boxes, 0 = 0