apply aux (m-1) (tail ⟨x::xs, _⟩)
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
no goals