no goals
α : Sort u_1
ctx : Context α
e : List Nat
⊢ evalList α ctx (removeNeutrals ctx e) = evalList α ctx e
induction e using List.two_step_induction with
| empty => rfl
| single =>
  simp [removeNeutrals, removeNeutrals.loop]; split
  case h_1 => rfl
  case h_2 h => split at h <;> simp_all
| step x y ys ih =>
  cases h₁ : ContextInformation.isNeutral ctx x <;> cases h₂ : ContextInformation.isNeutral ctx y <;> cases h₃ : removeNeutrals.loop ctx ys
  <;> simp [removeNeutrals, removeNeutrals.loop, h₁, h₂, h₃, evalList, ←ih]
  <;> (try simp [unwrap_isNeutral h₂ |>.2])
  <;> (try simp [unwrap_isNeutral h₁ |>.1])
no goals
case empty
α : Sort u_1
ctx : Context α
⊢ evalList α ctx (removeNeutrals ctx []) = evalList α ctx []
rfl
case single
α : Sort u_1
ctx : Context α
a✝ : Nat
⊢ evalList α ctx
      (match
        match ContextInformation.isNeutral ctx a✝ with
        | true => []
        | false => [a✝] with
      | [] => [a✝]
      | ys => ys) =
    evalList α ctx [a✝]
case single
α : Sort u_1
ctx : Context α
a✝ : Nat
⊢ evalList α ctx (removeNeutrals ctx [a✝]) = evalList α ctx [a✝]
simp [removeNeutrals, removeNeutrals.loop]
case single.h_1
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝ : List Nat
heq✝ :
  (match ContextInformation.isNeutral ctx a✝ with
    | true => []
    | false => [a✝]) =
    []
⊢ evalList α ctx [a✝] = evalList α ctx [a✝]

case single.h_2
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝¹ : List Nat
x✝ :
  (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
      [] →
    False
⊢ evalList α ctx
      (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
    evalList α ctx [a✝]
case single
α : Sort u_1
ctx : Context α
a✝ : Nat
⊢ evalList α ctx
      (match
        match ContextInformation.isNeutral ctx a✝ with
        | true => []
        | false => [a✝] with
      | [] => [a✝]
      | ys => ys) =
    evalList α ctx [a✝]
split
case single.h_2
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝¹ : List Nat
x✝ :
  (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
      [] →
    False
⊢ evalList α ctx
      (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
    evalList α ctx [a✝]
case single.h_1
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝ : List Nat
heq✝ :
  (match ContextInformation.isNeutral ctx a✝ with
    | true => []
    | false => [a✝]) =
    []
⊢ evalList α ctx [a✝] = evalList α ctx [a✝]

case single.h_2
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝¹ : List Nat
x✝ :
  (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
      [] →
    False
⊢ evalList α ctx
      (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
    evalList α ctx [a✝]
case h_1 => rfl
no goals
case single.h_2
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝¹ : List Nat
x✝ :
  (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
      [] →
    False
⊢ evalList α ctx
      (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
    evalList α ctx [a✝]
case h_2 h => split at h <;> simp_all
no goals
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝ : List Nat
heq✝ :
  (match ContextInformation.isNeutral ctx a✝ with
    | true => []
    | false => [a✝]) =
    []
⊢ evalList α ctx [a✝] = evalList α ctx [a✝]
rfl
no goals
α : Sort u_1
ctx : Context α
a✝ : Nat
x✝ : List Nat
h :
  (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
      [] →
    False
⊢ evalList α ctx
      (match ContextInformation.isNeutral ctx a✝ with
      | true => []
      | false => [a✝]) =
    evalList α ctx [a✝]
split at h <;> simp_all
no goals
case step
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
⊢ evalList α ctx (removeNeutrals ctx (x :: y :: ys)) = evalList α ctx (x :: y :: ys)
cases h₁ : ContextInformation.isNeutral ctx x <;> cases h₂ : ContextInformation.isNeutral ctx y <;> cases h₃ : removeNeutrals.loop ctx ys
<;> simp [removeNeutrals, removeNeutrals.loop, h₁, h₂, h₃, evalList, ←ih]
<;> (try simp [unwrap_isNeutral h₂ |>.2])
<;> (try simp [unwrap_isNeutral h₁ |>.1])
case step.true.true.cons
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
h₁ : ContextInformation.isNeutral ctx x = true
h₂ : ContextInformation.isNeutral ctx y = true
head✝ : Nat
tail✝ : List Nat
h₃ : removeNeutrals.loop ctx ys = head✝ :: tail✝
⊢ evalList α ctx (head✝ :: tail✝) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))
case step.true.true.cons
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
h₁ : ContextInformation.isNeutral ctx x = true
h₂ : ContextInformation.isNeutral ctx y = true
head✝ : Nat
tail✝ : List Nat
h₃ : removeNeutrals.loop ctx ys = head✝ :: tail✝
⊢ evalList α ctx (head✝ :: tail✝) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))
try simp [unwrap_isNeutral h₂ |>.2]
case step.true.true.cons
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
h₁ : ContextInformation.isNeutral ctx x = true
h₂ : ContextInformation.isNeutral ctx y = true
head✝ : Nat
tail✝ : List Nat
h₃ : removeNeutrals.loop ctx ys = head✝ :: tail✝
⊢ evalList α ctx (head✝ :: tail✝) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))
case step.true.true.cons
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
h₁ : ContextInformation.isNeutral ctx x = true
h₂ : ContextInformation.isNeutral ctx y = true
head✝ : Nat
tail✝ : List Nat
h₃ : removeNeutrals.loop ctx ys = head✝ :: tail✝
⊢ evalList α ctx (head✝ :: tail✝) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))
simp [unwrap_isNeutral h₂ |>.2]
no goals
case step.true.true.cons
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
h₁ : ContextInformation.isNeutral ctx x = true
h₂ : ContextInformation.isNeutral ctx y = true
head✝ : Nat
tail✝ : List Nat
h₃ : removeNeutrals.loop ctx ys = head✝ :: tail✝
⊢ evalList α ctx (head✝ :: tail✝) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))
try simp [unwrap_isNeutral h₁ |>.1]
no goals
case step.true.true.cons
α : Sort u_1
ctx : Context α
x y : Nat
ys : List Nat
ih : evalList α ctx (removeNeutrals ctx (y :: ys)) = evalList α ctx (y :: ys)
h₁ : ContextInformation.isNeutral ctx x = true
h₂ : ContextInformation.isNeutral ctx y = true
head✝ : Nat
tail✝ : List Nat
h₃ : removeNeutrals.loop ctx ys = head✝ :: tail✝
⊢ evalList α ctx (head✝ :: tail✝) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))
simp [unwrap_isNeutral h₁ |>.1]