rename_i neq h₁ h₂
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False