Theorems about ubyte64 and IHS functions.
Theorem: ubyte64p-of-loghead-of-64
(defthm ubyte64p-of-loghead-of-64 (ubyte64p (loghead 64 x)))
