fix: drop metadata on the arithmetic spine in the `Sym.Arith` normalizer

This PR fixes a panic in the `Sym.simp`-based `grind` normalizer on `match` equations whose patterns contain arithmetic, e.g. `grind [h.eq_def]` for a function matching on `Vec α (n + 1 + 1)`.

The conditions of `match` equations keep the `_inaccessible` annotation on pattern terms (`a = [mdata] n + 1 + 1`). `match_expr` sees through `Expr.mdata`, but the structural destructuring that followed it in `visitAtoms` and `canonArith` did not, so the annotated node was classified as an addition and then failed with `unreachable code` or `Expr.appFn!`. Metadata is transparent to the kernel and `grind` never internalizes it, so both functions now normalize the inner term and drop the wrapper.

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