no goals
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx (Expr.toList e) = eval α ctx e
induction e with
| var x => rfl
| op l r ih₁ ih₂ =>
  simp [evalList, Expr.toList, eval, ←ih₁, ←ih₂]
  apply evalList_append <;> apply toList_nonEmpty
no goals
case var
α : Sort u_1
ctx : Context α
x : Nat
⊢ evalList α ctx (Expr.toList (Expr.var x)) = eval α ctx (Expr.var x)
rfl
case op
α : Sort u_1
ctx : Context α
l r : Expr
ih₁ : evalList α ctx (Expr.toList l) = eval α ctx l
ih₂ : evalList α ctx (Expr.toList r) = eval α ctx r
⊢ evalList α ctx (Expr.toList l ++ Expr.toList r) =
    EvalInformation.evalOp ctx (evalList α ctx (Expr.toList l)) (evalList α ctx (Expr.toList r))
case op
α : Sort u_1
ctx : Context α
l r : Expr
ih₁ : evalList α ctx (Expr.toList l) = eval α ctx l
ih₂ : evalList α ctx (Expr.toList r) = eval α ctx r
⊢ evalList α ctx (Expr.toList (Expr.op l r)) = eval α ctx (Expr.op l r)
simp [evalList, Expr.toList, eval, ←ih₁, ←ih₂]
no goals
case op
α : Sort u_1
ctx : Context α
l r : Expr
ih₁ : evalList α ctx (Expr.toList l) = eval α ctx l
ih₂ : evalList α ctx (Expr.toList r) = eval α ctx r
⊢ evalList α ctx (Expr.toList l ++ Expr.toList r) =
    EvalInformation.evalOp ctx (evalList α ctx (Expr.toList l)) (evalList α ctx (Expr.toList r))
apply evalList_append <;> apply toList_nonEmpty