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