no goals
α : Sort u_1
ctx : Context α
l r : List Nat
h₁ : l ≠ []
h₂ : r ≠ []
⊢ evalList α ctx (List.append l r) = op ctx (evalList α ctx l) (evalList α ctx r)
induction l using List.two_step_induction with
| empty => simp_all
| single x =>
  cases r
  . simp at h₂
  . simp [List.append, evalList, EvalInformation.evalOp]
| step x y ys ih => simp [List.append, evalList, EvalInformation.evalOp] at *; rw [ih]; simp [ctx.assoc.1]
no goals
case empty
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : r ≠ []
h₁ : [] ≠ []
⊢ evalList α ctx (List.append [] r) = op ctx (evalList α ctx []) (evalList α ctx r)
simp_all
case single.nil
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
h₂ : [] ≠ []
⊢ evalList α ctx (List.append [x] []) = op ctx (evalList α ctx [x]) (evalList α ctx [])

case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx (List.append [x] (head✝ :: tail✝)) = op ctx (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))
case single
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : r ≠ []
x : Nat
h₁ : [x] ≠ []
⊢ evalList α ctx (List.append [x] r) = op ctx (evalList α ctx [x]) (evalList α ctx r)
cases r
case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx (List.append [x] (head✝ :: tail✝)) = op ctx (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))
case single.nil
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
h₂ : [] ≠ []
⊢ evalList α ctx (List.append [x] []) = op ctx (evalList α ctx [x]) (evalList α ctx [])

case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx (List.append [x] (head✝ :: tail✝)) = op ctx (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))
. simp at h₂
no goals
case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx (List.append [x] (head✝ :: tail✝)) = op ctx (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))
. simp [List.append, evalList, EvalInformation.evalOp]
no goals
case single.nil
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
h₂ : [] ≠ []
⊢ evalList α ctx (List.append [x] []) = op ctx (evalList α ctx [x]) (evalList α ctx [])
simp at h₂
no goals
case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx (List.append [x] (head✝ :: tail✝)) = op ctx (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))
simp [List.append, evalList, EvalInformation.evalOp]
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: (ys ++ r))) =
    op ctx (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : r ≠ []
x y : Nat
ys : List Nat
ih : y :: ys ≠ [] → evalList α ctx (List.append (y :: ys) r) = op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : x :: y :: ys ≠ []
⊢ evalList α ctx (List.append (x :: y :: ys) r) = op ctx (evalList α ctx (x :: y :: ys)) (evalList α ctx r)
simp [List.append, evalList, EvalInformation.evalOp] at *
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ op ctx (EvalInformation.evalVar ctx x) (op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)) =
    op ctx (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: (ys ++ r))) =
    op ctx (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)
rw [ih]
no goals
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ op ctx (EvalInformation.evalVar ctx x) (op ctx (evalList α ctx (y :: ys)) (evalList α ctx r)) =
    op ctx (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)
simp [ctx.assoc.1]