feat: `[grind hom fallback]` rules, tried only when no other homomorphism rule applies

This PR adds the `fallback` modifier to the `[grind hom]` attribute. A fallback rule is applied to a term only when no other homomorphism rule matches it, using the second tier `Sym.simp` already has for `eq_def` unfolding.

It is meant for rules whose left-hand side matches every application of an injection, such as a bridge `x.toInt = x.toBitVec.toInt` between two images of the same type: as an ordinary rule it takes precedence over more specific rules like `(a + b).toInt = ...`, since the rewriter applies the first matching rule. This PR only adds the mechanism; the bridge rules of the fixed-width signed integers are switched to it in a follow-up, once stage0 includes the attribute handler.

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