no goals
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (go k p) = k * denote ctx p
match p with
| [] => rfl
| (k', v) :: p => simp [Poly.mul.go, go_denote]
no goals
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (go k []) = k * denote ctx []
rfl
no goals
ctx : Context
k : Nat
p✝ : Poly
k' : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx (go k ((k', v) :: p)) = k * denote ctx ((k', v) :: p)
simp [Poly.mul.go, go_denote]