Theorems about sbyte8 and IHS functions.
Theorem: sbyte8p-of-logext-of-8
(defthm sbyte8p-of-logext-of-8 (sbyte8p (logext 8 x)))
