Homomorphism rules for BitVec used by the grind tactic.
The unsigned fragment is injected into Nat via BitVec.toNat, and the signed
fragment into Int via BitVec.toInt.
Homomorphism predicates: range facts for the injection functions, instantiated by
grind for the terms it internalizes. The 2 * toInt bounds are restated with an
explicit parameter, as required by the [grind hom_pred] trigger inference.