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

theorem Lean.Grind.Int64.toInt_eq_toBitVec_toInt (x : Int64) : x.toInt = x.toBitVec.toInt

Translations of ≤ and < into the target domain.