fix: mark `Grind.nestedDecidable` as an abbreviation

This PR fixes a performance issue where proof terms produced by `grind` could trigger kernel deterministic timeouts.
`grind` canonicalizes nested `Decidable` instances under the identity wrapper `Grind.nestedDecidable`, leaving the kernel to check
`t =?= Grind.nestedDecidable t`. The kernel does not see the `[reducible]` attribute, and its lazy-delta heuristic unfolded `t`
instead of the wrapper. When `t` is an instance such as `UInt32.decLe` applied to a symbolic argument and a large literal
(e.g., `97 ≤ c.val + 4294967264` coming from `Char`/`UInt32` wraparound), the check descended through `BitVec` and `Fin` into
`Nat.ble` on a `2^32`-sized literal with a free variable inside, where the fast numeral path does not apply, and effectively never terminated.
Marking `nestedDecidable` as an abbreviation stores the `abbrev` reducibility hint in the declaration itself, which the kernel does honor,
so the wrapper side is unfolded first and the check succeeds immediately.

The `unfoldReducible` preprocessor now treats `Grind.nestedDecidable` as a `grind` gadget that must not be unfolded: like `Grind.EqMatch` and `Grind.MatchCond`,
it is an `abbrev` that must survive until the corresponding propagators consume it.

Reported by Paul Reichert.
3 files changed