Theorems about value-integer and value-integer->get.
Theorem:
(defthm value-integer-of-value-integer->get-when-type-of-value (implies (and (value-integerp val) (equal type (type-of-value val))) (equal (value-integer (value-integer->get val) type) (value-fix val))))
Theorem:
(defthm value-integer->get-of-value-integer (b* ((val (value-integer mathint type))) (implies (and (type-nonchar-integerp type) (integer-type-rangep mathint type)) (equal (value-integer->get val) (ifix mathint)))))