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