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

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

Translations of ≤ and < into the target domain.