{motive_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof → Sort u} →
              {motive_8 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Sort u} →
                {motive_9 : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof → Sort u} →
                  {motive_10 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Sort u} →
                    {motive_11 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof → Sort u} →
                      {motive_12 : Lean.Meta.Grind.Arith.Cutsat.UnsatProof → Sort u} →
                        {motive_13 : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Sort u} →
                          {motive_14 : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
                            {motive_15 : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Sort u} →
                              {motive_16 : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof) → Sort u} →
                                {motive_17 : List (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Sort u} →
                                  {motive_18 : List (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof) → Sort u} →
                                    {motive_19 : Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
                                      {motive_20 : Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof → Sort u} →
                                        {motive_21 : ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
                                          Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Sort (max 1 u)