∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)), i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q