Alternative definition of value-promoted-arithmeticp, in terms of the shallow embedding's integer value recognizers.
Theorem:
(defthm value-promoted-arithmeticp-alt-def (implies (valuep val) (equal (value-promoted-arithmeticp val) (or (uintp val) (sintp val) (ulongp val) (slongp val) (ullongp val) (sllongp val)))))