cases contr
n : ℕ
a b : Variables n order.GrLex
contr : Order.lex a b ∨ Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
case inl
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
⊢ Order.grlex a b ∨ Order.grlex b a

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a