no goals
α : Sort u_1
y : Nat
ctx : Context α
h : IsCommutative ctx.op
xs ys : List Nat
⊢ evalList α ctx (sort.loop xs (y :: ys)) = evalList α ctx (sort.loop (y :: xs) ys)
induction ys generalizing y xs with
| nil => simp [sort.loop, evalList_insert ctx h]
| cons z zs _  =>
  simp [sort.loop]; apply evalList_sort_congr ctx h
  simp [evalList_insert ctx h]
  cases h₂ : insert y xs
  . apply absurd h₂; simp [insert_nonEmpty]
  . simp [evalList, ←h₂, evalList_insert ctx h]
  all_goals simp [insert_nonEmpty]
no goals
case nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
y : Nat
xs : List Nat
⊢ evalList α ctx (sort.loop xs [y]) = evalList α ctx (sort.loop (y :: xs) [])
simp [sort.loop, evalList_insert ctx h]
case cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (sort.loop (insert z (insert y xs)) zs) = evalList α ctx (sort.loop (insert z (y :: xs)) zs)
case cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (sort.loop xs (y :: z :: zs)) = evalList α ctx (sort.loop (y :: xs) (z :: zs))
simp [sort.loop]
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (insert z (insert y xs)) = evalList α ctx (insert z (y :: xs))

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
case cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (sort.loop (insert z (insert y xs)) zs) = evalList α ctx (sort.loop (insert z (y :: xs)) zs)
apply evalList_sort_congr ctx h
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (z :: insert y xs) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (insert z (insert y xs)) = evalList α ctx (insert z (y :: xs))

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
simp [evalList_insert ctx h]
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ evalList α ctx [z] = evalList α ctx (z :: y :: xs)

case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (z :: insert y xs) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
cases h₂ : insert y xs
case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ evalList α ctx [z] = evalList α ctx (z :: y :: xs)

case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
. apply absurd h₂; simp [insert_nonEmpty]
case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
. simp [evalList, ←h₂, evalList_insert ctx h]
no goals
case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
all_goals simp [insert_nonEmpty]
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ ¬insert y xs = []
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ evalList α ctx [z] = evalList α ctx (z :: y :: xs)
apply absurd h₂
no goals
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ ¬insert y xs = []
simp [insert_nonEmpty]
no goals
case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)
simp [evalList, ←h₂, evalList_insert ctx h]
no goals
case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []
simp [insert_nonEmpty]