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

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

Translations of ≤ and < into the target domain.