(motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) →
  (w : ℕ) →
    (expr : Std.Tactic.BVDecide.BVExpr w) →
      ((w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a)) →
        ((w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val)) →
          ((w : ℕ) →
              (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
                (op : Std.Tactic.BVDecide.BVBinOp) →
                  (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr)) →
            ((w : ℕ) →
                (op : Std.Tactic.BVDecide.BVUnOp) →
                  (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr)) →
              ((w l r : ℕ) →
                  (lhs : Std.Tactic.BVDecide.BVExpr l) →
                    (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h)) →
                ((w w_1 n : ℕ) →
                    (expr : Std.Tactic.BVDecide.BVExpr w_1) →
                      (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h)) →
                  ((len w start : ℕ) →
                      (expr : Std.Tactic.BVDecide.BVExpr w) →
                        motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr)) →
                    ((w n : ℕ) →
                        (lhs : Std.Tactic.BVDecide.BVExpr w) →
                          (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs)) →
                      ((w n : ℕ) →
                          (lhs : Std.Tactic.BVDecide.BVExpr w) →
                            (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs)) →
                        ((w n : ℕ) →
                            (lhs : Std.Tactic.BVDecide.BVExpr w) →
                              (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)) →
                          motive w expr