Alternative definition of value-signed-integerp, in terms of the shallow embedding's integer value recognizers.
Theorem:
(defthm value-signed-integerp-alt-def (equal (value-signed-integerp val) (b* ((val (value-fix val))) (or (scharp val) (sshortp val) (sintp val) (slongp val) (sllongp val)))))