rename_i eq _ _ neq
case inr.inr.inl.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 a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case 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 a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
case inr.inr.inl.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
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case 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 a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False