∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : Lean.Compiler.LCNF.Code pu)
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 = F_4 t (Lean.Compiler.LCNF.Code.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6).2