match v with 
  | ⟨[], p⟩    => rw [Order.lex_impl]
                  split
                  simp at *
                  simp at p
                  simp at *                                   
  | ⟨x::xs, _⟩ => rw [Order.lex_impl]
                  split
                  simp
                  simp at *
                  simp at *
                  simp [Nat.le_refl]
                  rename_i x₁ _ x₂ _ h₁ h₂
                  have h₃ := Eq.symm h₁.left
                  have h₄ := Eq.symm h₂.left
                  rw [h₃, h₄]
                  simp [Nat.le_refl]
                  apply aux (m-1) (tail ⟨x::xs, _⟩)
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
⊢ Order.lex_impl v v
no goals