Theorems about sbyte16 and IHS functions.
Theorem: sbyte16p-of-logext-of-16
(defthm sbyte16p-of-logext-of-16 (sbyte16p (logext 16 x)))
