∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} (t : Lean.Elab.Term.Do.Code)
  (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 = F_1 t (Lean.Elab.Term.Do.Code.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2