fix: ignore heterogeneous equalities in `grind hom` solver hooks (#14769)

This PR fixes an internal `grind` error (`mkEqProof` invoked with terms
of different types). An equivalence class can contain terms of different
types when they are merged via `HEq` (e.g., `BitVec` terms of different
widths related through `cast` terms). The `=`-injection performed by the
`[grind hom]` hooks applies only to homogeneous equalities, so
`processNewEq` and `processNewDiseq` now skip pairs whose types differ.

It also repairs the `grind_bitvec2` benchmark, which was broken by the
eager homomorphism encoding: it removes a redundant `grind_pattern`
subsumed by `[grind hom]` whose instances were exhausting the case-split
budget, and increases the split budget in one proof that needs a
model-based theory combination case split to find the exponent identity
`w + w * n = w * (n + 1)`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>