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

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

Translations of ≤ and < into the target domain.