{motive : Lean.Elab.Tactic.BVDecide.Frontend.SolverMode → Sort u} →
  (t : Lean.Elab.Tactic.BVDecide.Frontend.SolverMode) →
    motive Lean.Elab.Tactic.BVDecide.Frontend.SolverMode.proof →
      motive Lean.Elab.Tactic.BVDecide.Frontend.SolverMode.counterexample →
        motive Lean.Elab.Tactic.BVDecide.Frontend.SolverMode.default → motive t