Theorem: unsigned-byte-p-lshu
(defthm unsigned-byte-p-lshu (implies (and (>= size1 size) (>= size 0) (integerp size) (integerp size1)) (unsigned-byte-p size1 (lshu size i cnt))))
