∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (BoxIntegral.Box ι)) (le_of_mem' : ∀ J ∈ boxes, J ≤ I)
  (pairwiseDisjoint : (↑boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet))
  (boxes_1 : Finset (BoxIntegral.Box ι)) (le_of_mem'_1 : ∀ J ∈ boxes_1, J ≤ I)
  (pairwiseDisjoint_1 : (↑boxes_1).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)),
  ({ boxes := boxes, le_of_mem' := le_of_mem', pairwiseDisjoint := pairwiseDisjoint } =
      { boxes := boxes_1, le_of_mem' := le_of_mem'_1, pairwiseDisjoint := pairwiseDisjoint_1 }) =
    (boxes = boxes_1)