Theorems about ubyte5 and IHS functions.
Theorem: ubyte5p-of-loghead-of-5
(defthm ubyte5p-of-loghead-of-5 (ubyte5p (loghead 5 x)))
Theorem: loghead-of-5-when-ubyte5p
(defthm loghead-of-5-when-ubyte5p (implies (ubyte5p x) (equal (loghead 5 x) x)))
