exact heq₁
case inl.inl.left
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ x = y

case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }