∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.Box ι → M)
  (h :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I₀ → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, f Ji = f J),
  ⇑{ toFun := f, sum_partition_boxes' := h } = f