(motive :
    Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr × Array (ℤ × Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
      Sort u_1) →
  (x : Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr × Array (ℤ × Lean.Meta.Grind.Arith.Linear.IneqCnstr)) →
    ((lowers' : Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
        (todo : Array (ℤ × Lean.Meta.Grind.Arith.Linear.IneqCnstr)) → motive (lowers', todo)) →
      motive x