{motive_1 : Lean.Compiler.LCNF.UnreachableBranches.Value → Sort u} →
  (t : Lean.Compiler.LCNF.UnreachableBranches.Value) →
    motive_1 Lean.Compiler.LCNF.UnreachableBranches.Value.bot →
      motive_1 Lean.Compiler.LCNF.UnreachableBranches.Value.top →
        ((i : Lean.Name) →
            (vs : Array Lean.Compiler.LCNF.UnreachableBranches.Value) →
              motive_1 (Lean.Compiler.LCNF.UnreachableBranches.Value.ctor i vs)) →
          ((vs : List Lean.Compiler.LCNF.UnreachableBranches.Value) →
              motive_1 (Lean.Compiler.LCNF.UnreachableBranches.Value.choice vs)) →
            motive_1 t