no goals
ctx : Context
p q : Poly
⊢ denote ctx (p ++ q) = denote ctx p + denote ctx q
match p with
| []  => simp
| (k, v) :: p => simp [denote_append]
no goals
ctx : Context
p q : Poly
⊢ denote ctx ([] ++ q) = denote ctx [] + denote ctx q
simp
no goals
ctx : Context
p✝ q : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx ((k, v) :: p ++ q) = denote ctx ((k, v) :: p) + denote ctx q
simp [denote_append]