Homomorphism rules for UInt32 used by the grind tactic. The injection function is UInt32.toBitVec.

theorem Lean.Grind.UInt32.toNat_eq_toBitVec_toNat (x : UInt32) : x.toNat = x.toBitVec.toNat

Translations of ≤ and < into the target domain.