no goals
ctx : Context
e : Expr
p : Poly
⊢ Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
induction p generalizing e with
| nil => simp [toExpr.go, Poly.denote]
| cons kv p ih => cases kv; simp [toExpr.go, ih, Expr.denote, Poly.denote]
no goals
case nil
ctx : Context
e : Expr
⊢ Expr.denote ctx (toExpr.go e []) = Expr.denote ctx e + denote ctx []
simp [toExpr.go, Poly.denote]
case cons.mk
ctx : Context
p : List (Nat × Var)
ih : ∀ (e : Expr), Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
e : Expr
fst✝ : Nat
snd✝ : Var
⊢ Expr.denote ctx (toExpr.go e ((fst✝, snd✝) :: p)) = Expr.denote ctx e + denote ctx ((fst✝, snd✝) :: p)
case cons
ctx : Context
kv : Nat × Var
p : List (Nat × Var)
ih : ∀ (e : Expr), Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
e : Expr
⊢ Expr.denote ctx (toExpr.go e (kv :: p)) = Expr.denote ctx e + denote ctx (kv :: p)
cases kv
no goals
case cons.mk
ctx : Context
p : List (Nat × Var)
ih : ∀ (e : Expr), Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
e : Expr
fst✝ : Nat
snd✝ : Var
⊢ Expr.denote ctx (toExpr.go e ((fst✝, snd✝) :: p)) = Expr.denote ctx e + denote ctx ((fst✝, snd✝) :: p)
simp [toExpr.go, ih, Expr.denote, Poly.denote]