{n : ℕ} →
  {G : Type u} →
    [inst : AddCommGroup G] →
      (I₀ : BoxIntegral.Box (Fin (n + 1))) →
        (i : Fin (n + 1)) →
          (f : ℝ → BoxIntegral.Box (Fin n) → G) →
            (fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → BoxIntegral.BoxAdditiveMap (Fin n) G ↑(I₀.face i)) →
              (∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : BoxIntegral.Box (Fin n)),
                  f x J = (fb ⟨x, hx⟩) J) →
                BoxIntegral.BoxAdditiveMap (Fin (n + 1)) G ↑I₀