`bv_decide`: better failure message

bv_decide currently generates error messages such as

None of the hypotheses are in the supported BitVec fragment.
There are two potential fixes for this:
1. If you are using custom BitVec constructs simplify them to built-in ones.
2. If your problem is using only built-in ones it might currently be out of reach.
   Consider expressing it in terms of different operations that are better supported.

We should include the term that triggered the error message. Otherwise, it may be quite hard to diagnose the issue.
Here is an example that triggers this issue.

theorem ushiftRight_symbolic_shift (x : BitVec 64) (n : Nat) (h : n < 64) :
  x >>> n = (BitVec.extractLsb 63 n x).zeroExtend 64 := by
  bv_decide

Start by reproducing the ushiftRight_symbolic_shift theorem and its bv_decide failure. Trace where the unsupported BitVec-fragment diagnostic is produced, then update it so the triggering term is included; the example should produce a more actionable message when the change is done.