∀ {ι : Type u_1} {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι),
  (∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J) →
    (∀ z ∈ BoxIntegral.Box.Icc I,
        ∃ U ∈ nhdsWithin z (BoxIntegral.Box.Icc I),
          ∀ J ≤ I,
            ∀ (m : ℕ),
              z ∈ BoxIntegral.Box.Icc J →
                BoxIntegral.Box.Icc J ⊆ U →
                  (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) →
      p I