Theorems about ubyte8 and IHS functions.
Theorem: ubyte8p-of-loghead-of-8
(defthm ubyte8p-of-loghead-of-8 (ubyte8p (loghead 8 x)))
