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