∀ {motive_1 : Lean.Compiler.LCNF.UnreachableBranches.Value → Sort u}
  {motive_2 : Array Lean.Compiler.LCNF.UnreachableBranches.Value → Sort u}
  {motive_3 : List Lean.Compiler.LCNF.UnreachableBranches.Value → Sort u}
  (t : Array Lean.Compiler.LCNF.UnreachableBranches.Value)
  (F_1 : (t : Lean.Compiler.LCNF.UnreachableBranches.Value) → t.below → motive_1 t)
  (F_2 :
    (t : Array Lean.Compiler.LCNF.UnreachableBranches.Value) →
      Lean.Compiler.LCNF.UnreachableBranches.Value.below_1 t → motive_2 t)
  (F_3 :
    (t : List Lean.Compiler.LCNF.UnreachableBranches.Value) →
      Lean.Compiler.LCNF.UnreachableBranches.Value.below_2 t → motive_3 t),
  Lean.Compiler.LCNF.UnreachableBranches.Value.brecOn_1 t F_1 F_2 F_3 =
    F_2 t (Lean.Compiler.LCNF.UnreachableBranches.Value.brecOn_1.go t F_1 F_2 F_3).2