no goals
α : Sort u_1
a b c : List Nat
ctx : Context α
h : IsCommutative ctx.op
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop a c) = evalList α ctx (sort.loop b c)
induction c generalizing a b with
| nil => simp [sort.loop, h₂]
| cons c _  ih =>
  simp [sort.loop]; apply ih; simp [evalList_insert ctx h, evalList]
  cases a with
  | nil => apply absurd h₃; simp
  | cons a as =>
    cases b with
    | nil => apply absurd h₄; simp
    | cons b bs => simp [evalList, h₂]
  all_goals apply insert_nonEmpty
no goals
case nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop a []) = evalList α ctx (sort.loop b [])
simp [sort.loop, h₂]
case cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop (insert c a) tail✝) = evalList α ctx (sort.loop (insert c b) tail✝)
case cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop a (c :: tail✝)) = evalList α ctx (sort.loop b (c :: tail✝))
simp [sort.loop]
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (insert c a) = evalList α ctx (insert c b)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
case cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop (insert c a) tail✝) = evalList α ctx (sort.loop (insert c b) tail✝)
apply ih
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (c :: a) = evalList α ctx (c :: b)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (insert c a) = evalList α ctx (insert c b)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
simp [evalList_insert ctx h, evalList]
case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
case cons.h₂
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (c :: a) = evalList α ctx (c :: b)

case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
cases a with
| nil => apply absurd h₃; simp
| cons a as =>
  cases b with
  | nil => apply absurd h₄; simp
  | cons b bs => simp [evalList, h₂]
no goals
case cons.h₃
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
all_goals apply insert_nonEmpty
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
h₂ : evalList α ctx [] = evalList α ctx b
h₃ : [] ≠ []
⊢ ¬[] ≠ []
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
h₂ : evalList α ctx [] = evalList α ctx b
h₃ : [] ≠ []
⊢ evalList α ctx [c] = evalList α ctx (c :: b)
apply absurd h₃
no goals
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
h₂ : evalList α ctx [] = evalList α ctx b
h₃ : [] ≠ []
⊢ ¬[] ≠ []
simp
no goals
case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
a : Nat
as : List Nat
h₂ : evalList α ctx (a :: as) = evalList α ctx b
h₃ : a :: as ≠ []
⊢ evalList α ctx (c :: a :: as) = evalList α ctx (c :: b)
cases b with
| nil => apply absurd h₄; simp
| cons b bs => simp [evalList, h₂]
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
h₄ : [] ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx []
⊢ ¬[] ≠ []
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
h₄ : [] ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx []
⊢ evalList α ctx (c :: a :: as) = evalList α ctx [c]
apply absurd h₄
no goals
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
h₄ : [] ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx []
⊢ ¬[] ≠ []
simp
no goals
case cons.h₂.cons.cons
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
b : Nat
bs : List Nat
h₄ : b :: bs ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx (b :: bs)
⊢ evalList α ctx (c :: a :: as) = evalList α ctx (c :: b :: bs)
simp [evalList, h₂]
no goals
case cons.h₄
α : Sort u_1
ctx : Context α
h : IsCommutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []
apply insert_nonEmpty