Possible integer and other predicates for values.
Theorem:
(defthm valuep-possibilities (implies (valuep x) (or (ucharp x) (scharp x) (ushortp x) (sshortp x) (uintp x) (sintp x) (ulongp x) (slongp x) (ullongp x) (sllongp x) (value-case x :pointer) (value-case x :array) (value-case x :struct))) :rule-classes :forward-chaining)