match a, b with
  | ⟨[], p⟩, ⟨[], q⟩       => simp 
  | ⟨x::xs, p⟩, ⟨y::ys, q⟩ => rw [Order.lex_impl] at ab ba
                              simp at *
                              split at ab
                              split at ba
                              rename_i heq₁ heq₂
                              simp [Vector]
                              constructor
                              exact heq₁ 
                              have eq := aux (m-1) (tail ⟨x::xs, p⟩) (tail ⟨y::ys, q⟩) ab ba
                              simp [tail, Vector] at eq
                              exact eq
                              rename_i eq neq
                              have eq_symm := Eq.symm eq
                              contradiction
                              split at ba
                              rename_i neq eq
                              have eq_symm := Eq.symm eq
                              contradiction
                              rename_i neq₁ neq₂
                              have eq := Nat.le_antisymm ab ba
                              contradiction
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
ab : Order.lex_impl a b
ba : Order.lex_impl b a
⊢ a = b
no goals