simp [lex_le_refl]
case inl
n : ℕ
a : Variables n order.GrLex
h✝ : Order.lex a a
⊢ True

case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False
case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False