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

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

Translations of ≤ and < into the target domain.