(motive : Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred → Sort u_1) →
  (__discr : Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred) →
    ((pred : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred) → motive (some pred)) →
      ((x : Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred) → motive x) → motive __discr