Theorems about sbyte32 and IHS functions.
Theorem: sbyte32p-of-logext-of-32
(defthm sbyte32p-of-logext-of-32 (sbyte32p (logext 32 x)))
