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

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

Translations of ≤ and < into the target domain.