fix: normalize `BitVec.ofNat w k` literals with symbolic width in `grind`

This PR makes `grind` put `k#w` literals with a symbolic width `w` in the `OfNat.ofNat` form it uses for `BitVec` literals, so with the `Sym.simp`-based normalizer theorems such as `BitVec.sdiv_zero` apply to `x.sdiv 0` as they do with the legacy normalizer.

`Sym.Simp.evalGround` and `Sym.Canon.normNumLit?` only converted `BitVec.ofNat` literals with a literal width. They now convert symbolic widths too, so patterns, hypotheses, and the AC identity element `0#w` all reach the same `OfNat.ofNat` form.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>