-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.brecOn_4.eq : ∀ {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 : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof))
  (F_1 : (t : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Cutsat.CooperSplit) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof) → t.below → motive_7 t)
  (F_8 : (t : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) → t.below → motive_8 t)
  (F_9 : (t : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof) → t.below → motive_9 t)
  (F_10 : (t : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) → t.below → motive_10 t)
  (F_11 : (t : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof) → t.below → motive_11 t)
  (F_12 : (t : Lean.Meta.Grind.Arith.Cutsat.UnsatProof) → t.below → motive_12 t)
  (F_13 :
    (t : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) →
      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_1 t → motive_13 t)
  (F_14 :
    (t : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_2 t → motive_14 t)
  (F_15 :
    (t : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) → Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_3 t → motive_15 t)
  (F_16 :
    (t : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) →
      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_4 t → motive_16 t)
  (F_17 :
    (t : List (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) →
      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_5 t → motive_17 t)
  (F_18 :
    (t : List (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) →
      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_6 t → motive_18 t)
  (F_19 :
    (t : Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_7 t → motive_19 t)
  (F_20 :
    (t : Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof) →
      Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_8 t → motive_20 t)
  (F_21 :
    (t : ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Lean.Meta.Grind.Arith.Cutsat.EqCnstr.below_9 t → motive_21 t),
  Lean.Meta.Grind.Arith.Cutsat.EqCnstr.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 F_14 F_15 F_16
      F_17 F_18 F_19 F_20 F_21 =
    F_16 t
      (Lean.Meta.Grind.Arith.Cutsat.EqCnstr.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 F_14
          F_15 F_16 F_17 F_18 F_19 F_20 F_21).2