no goals
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx (p₁ ++ p₂) = denote ctx p₁ + denote ctx p₂
match p₁ with
| [] => simp!
| v :: p₁ => simp! [append_denote _ p₁ p₂, Nat.add_assoc]
no goals
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx ([] ++ p₂) = denote ctx [] + denote ctx p₂
simp!
no goals
ctx : Context
p₁✝ p₂ : Poly
v : Nat × Mon
p₁ : List (Nat × Mon)
⊢ denote ctx (v :: p₁ ++ p₂) = denote ctx (v :: p₁) + denote ctx p₂
simp! [append_denote _ p₁ p₂, Nat.add_assoc]