Alternative definition of value-unsigned-integerp, in terms of the shallow embedding's integer value recognizers.
Theorem:
(defthm value-unsigned-integerp-alt-def (equal (value-unsigned-integerp val) (b* ((val (value-fix val))) (or (ucharp val) (ushortp val) (uintp val) (ulongp val) (ullongp val)))))