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

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

Translations of ≤ and < into the target domain.