no goals
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x : Nat
xs : List Nat
⊢ evalList α ctx (insert x xs) = evalList α ctx (x :: xs)
induction xs using List.two_step_induction with
| empty => rfl
| single =>
  simp [insert]
  split
  . rfl
  . simp [evalList, h.1, EvalInformation.evalOp]
| step y z zs ih =>
  simp [insert] at *; split
  case inl => rfl
  case inr =>
    split
    case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
    case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
no goals
case empty
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x : Nat
⊢ evalList α ctx (insert x []) = evalList α ctx [x]
rfl
case single
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
⊢ evalList α ctx (if x < a✝ then [x, a✝] else [a✝, x]) = evalList α ctx [x, a✝]
case single
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
⊢ evalList α ctx (insert x [a✝]) = evalList α ctx [x, a✝]
simp [insert]
case single.inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : x < a✝
⊢ evalList α ctx [x, a✝] = evalList α ctx [x, a✝]

case single.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]
case single
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
⊢ evalList α ctx (if x < a✝ then [x, a✝] else [a✝, x]) = evalList α ctx [x, a✝]
split
case single.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]
case single.inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : x < a✝
⊢ evalList α ctx [x, a✝] = evalList α ctx [x, a✝]

case single.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]
. rfl
no goals
case single.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]
. simp [evalList, h.1, EvalInformation.evalOp]
no goals
case single.inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : x < a✝
⊢ evalList α ctx [x, a✝] = evalList α ctx [x, a✝]
rfl
no goals
case single.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]
simp [evalList, h.1, EvalInformation.evalOp]
case step
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
⊢ evalList α ctx (if x < y then x :: y :: z :: zs else y :: if x < z then x :: z :: zs else z :: insert x zs) =
    evalList α ctx (x :: y :: z :: zs)
case step
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (insert x (z :: zs)) = evalList α ctx (x :: z :: zs)
⊢ evalList α ctx (insert x (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
simp [insert] at *
case step.inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : x < y
⊢ evalList α ctx (x :: y :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

case step.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case step
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
⊢ evalList α ctx (if x < y then x :: y :: z :: zs else y :: if x < z then x :: z :: zs else z :: insert x zs) =
    evalList α ctx (x :: y :: z :: zs)
split
case step.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case step.inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : x < y
⊢ evalList α ctx (x :: y :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

case step.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case inl => rfl
no goals
case step.inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case inr =>
  split
  case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
  case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
no goals
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : x < y
⊢ evalList α ctx (x :: y :: z :: zs) = evalList α ctx (x :: y :: z :: zs)
rfl
case inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ evalList α ctx (y :: x :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

case inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
split
case inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case inl
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ evalList α ctx (y :: x :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

case inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
no goals
case inr
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ op ctx (EvalInformation.evalVar ctx y) (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    op ctx (EvalInformation.evalVar ctx x) (op ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ evalList α ctx (y :: x :: z :: zs) = evalList α ctx (x :: y :: z :: zs)
simp [evalList, EvalInformation.evalOp]
no goals
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ op ctx (EvalInformation.evalVar ctx y) (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    op ctx (EvalInformation.evalVar ctx x) (op ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))
rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (z :: insert x zs) = op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ op ctx (EvalInformation.evalVar ctx y) (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    op ctx (EvalInformation.evalVar ctx x) (op ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)
simp_all [evalList, EvalInformation.evalOp]
no goals
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (z :: insert x zs) = op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ op ctx (EvalInformation.evalVar ctx y) (op ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    op ctx (EvalInformation.evalVar ctx x) (op ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))
rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]