{motive : (a : ℕ) → Std.Tactic.BVDecide.BVExpr._impl a → Sort u} →
  ((hashCode : UInt64) → {w : ℕ} → (idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var._impl hashCode idx)) →
    ((hashCode : UInt64) →
        {w : ℕ} → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const._impl hashCode val)) →
      ((hashCode : UInt64) →
          {w : ℕ} →
            (start len : ℕ) →
              (expr : Std.Tactic.BVDecide.BVExpr w) →
                motive len (Std.Tactic.BVDecide.BVExpr.extract._impl hashCode start len expr)) →
        ((hashCode : UInt64) →
            {w : ℕ} →
              (lhs : Std.Tactic.BVDecide.BVExpr w) →
                (op : Std.Tactic.BVDecide.BVBinOp) →
                  (rhs : Std.Tactic.BVDecide.BVExpr w) →
                    motive w (Std.Tactic.BVDecide.BVExpr.bin._impl hashCode lhs op rhs)) →
          ((hashCode : UInt64) →
              {w : ℕ} →
                (op : Std.Tactic.BVDecide.BVUnOp) →
                  (operand : Std.Tactic.BVDecide.BVExpr w) →
                    motive w (Std.Tactic.BVDecide.BVExpr.un._impl hashCode op operand)) →
            ((hashCode : UInt64) →
                {l r w : ℕ} →
                  (lhs : Std.Tactic.BVDecide.BVExpr l) →
                    (rhs : Std.Tactic.BVDecide.BVExpr r) →
                      (h : w = l + r) → motive w (Std.Tactic.BVDecide.BVExpr.append._impl hashCode lhs rhs h)) →
              ((hashCode : UInt64) →
                  {w w' : ℕ} →
                    (n : ℕ) →
                      (expr : Std.Tactic.BVDecide.BVExpr w) →
                        (h : w' = w * n) → motive w' (Std.Tactic.BVDecide.BVExpr.replicate._impl hashCode n expr h)) →
                ((hashCode : UInt64) →
                    {m n : ℕ} →
                      (lhs : Std.Tactic.BVDecide.BVExpr m) →
                        (rhs : Std.Tactic.BVDecide.BVExpr n) →
                          motive m (Std.Tactic.BVDecide.BVExpr.shiftLeft._impl hashCode lhs rhs)) →
                  ((hashCode : UInt64) →
                      {m n : ℕ} →
                        (lhs : Std.Tactic.BVDecide.BVExpr m) →
                          (rhs : Std.Tactic.BVDecide.BVExpr n) →
                            motive m (Std.Tactic.BVDecide.BVExpr.shiftRight._impl hashCode lhs rhs)) →
                    ((hashCode : UInt64) →
                        {m n : ℕ} →
                          (lhs : Std.Tactic.BVDecide.BVExpr m) →
                            (rhs : Std.Tactic.BVDecide.BVExpr n) →
                              motive m (Std.Tactic.BVDecide.BVExpr.arithShiftRight._impl hashCode lhs rhs)) →
                      {a : ℕ} → (t : Std.Tactic.BVDecide.BVExpr._impl a) → motive a t