fix: interpret literals in `grind` only when their type is in normal form

This PR fixes `grind` producing a proof the kernel rejects (`decide (1 = 1) = false`) when the same literal occurs at definitionally equal but syntactically different types, such as `(1 : BitVec w)` and `(1 : BitVec 32)` for `@[implicit_reducible] def w : Nat := 32`.

`LitValues` recognizes literals up to `whnfD` on their types, so `(1 : BitVec w)` was an interpreted term with the same value as `(1 : BitVec 32)`. The canonicalizer runs at reducible transparency and does not unfold `w`, so the two remained distinct interpreted nodes in the E-graph. When model-based theory combination proposed equating them, `addEqStep` treated them as distinct values and `closeGoalWithValuesEq` built an invalid proof. With a semireducible `w`, the same path failed earlier with `failed to synthesize Decidable (1 = 1)`.

`isInterpreted` now requires the literal's type to be, structurally, a literal type with a normal form: `Nat`, `Int`, `String`, `Char`, `UInt8`, `UInt16`, `UInt32`, `UInt64`, or `Fin n`/`BitVec n` where `n` is a numeral. This also subsumes the explicit `Float`/`Float32` exclusion, since those types are not in the list.

Closes #15541

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>