∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  (f f_1 : BoxIntegral.BoxAdditiveMap ι M I₀),
  f = f_1 → ∀ (I : WithTop (BoxIntegral.Box ι)) (hI : I ≤ I₀), f.restrict I hI = f_1.restrict I hI