-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.brecOn.go : {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} →
                                          (t : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof) →
                                            ((t : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → t.below → motive_1 t) →
                                              ((t : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof) → t.below → motive_2 t) →
                                                ((t : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) → t.below → motive_3 t) →
                                                  ((t : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred) →
                                                      t.below → motive_4 t) →
                                                    ((t : Lean.Meta.Grind.Arith.Cutsat.CooperSplit) →
                                                        t.below → motive_5 t) →
                                                      ((t : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof) →
                                                          t.below → motive_6 t) →
                                                        ((t : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof) →
                                                            t.below → motive_7 t) →
                                                          ((t : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) →
                                                              t.below → motive_8 t) →
                                                            ((t : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof) →
                                                                t.below → motive_9 t) →
                                                              ((t : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) →
                                                                  t.below → motive_10 t) →
                                                                ((t : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof) →
                                                                    t.below → motive_11 t) →
                                                                  ((t : Lean.Meta.Grind.Arith.Cutsat.UnsatProof) →
                                                                      t.below → motive_12 t) →
                                                                    ((t :
                                                                          Array
                                                                            (Lean.Expr ×
                                                                              ℤ ×
                                                                                Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) →
                                                                        Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_1 t →
                                                                          motive_13 t) →
                                                                      ((t :
                                                                            Option
                                                                              Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                          Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_2
                                                                              t →
                                                                            motive_14 t) →
                                                                        ((t :
                                                                              Option
                                                                                Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                                                            Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_3
                                                                                t →
                                                                              motive_15 t) →
                                                                          ((t :
                                                                                Array
                                                                                  (Lean.FVarId ×
                                                                                    Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) →
                                                                              Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_4
                                                                                  t →
                                                                                motive_16 t) →
                                                                            ((t :
                                                                                  List
                                                                                    (Lean.Expr ×
                                                                                      ℤ ×
                                                                                        Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) →
                                                                                Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_5
                                                                                    t →
                                                                                  motive_17 t) →
                                                                              ((t :
                                                                                    List
                                                                                      (Lean.FVarId ×
                                                                                        Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) →
                                                                                  Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_6
                                                                                      t →
                                                                                    motive_18 t) →
                                                                                ((t :
                                                                                      Lean.Expr ×
                                                                                        ℤ ×
                                                                                          Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                                    Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_7
                                                                                        t →
                                                                                      motive_19 t) →
                                                                                  ((t :
                                                                                        Lean.FVarId ×
                                                                                          Lean.Meta.Grind.Arith.Cutsat.UnsatProof) →
                                                                                      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_8
                                                                                          t →
                                                                                        motive_20 t) →
                                                                                    ((t :
                                                                                          ℤ ×
                                                                                            Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                                        Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_9
                                                                                            t →
                                                                                          motive_21 t) →
                                                                                      motive_2 t ×' t.below