∀ (ctx : Nat.Linear.Context) (k : ℕ) (v : Nat.Linear.Var) (p : Nat.Linear.Poly),
  Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.insert k v p) =
    Nat.Linear.Poly.denote ctx p + k * Nat.Linear.Var.denote ctx v