Theorems about ubyte32 and IHS functions.
Theorem: ubyte32p-of-loghead-of-32
(defthm ubyte32p-of-loghead-of-32 (ubyte32p (loghead 32 x)))
