no goals
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx ((k, v) :: p) = k * Var.denote ctx v + denote ctx p
match p with
| []     => simp
| _ :: m => simp [denote_cons]
no goals
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx [(k, v)] = k * Var.denote ctx v + denote ctx []
simp
no goals
ctx : Context
k : Nat
v : Var
p : Poly
head✝ : Nat × Var
m : List (Nat × Var)
⊢ denote ctx ((k, v) :: head✝ :: m) = k * Var.denote ctx v + denote ctx (head✝ :: m)
simp [denote_cons]