Inversion theorems about the mappings between integer types and fixtype symbols.
Theorem:
(defthm fixtype-to-integer-type-of-integer-type-to-fixtype (implies (type-nonchar-integerp type) (equal (fixtype-to-integer-type (integer-type-to-fixtype type)) (type-fix type))))
Theorem:
(defthm integer-type-to-fixtype-of-fixtype-to-integer-type (implies (member-eq fixtype *nonchar-integer-fixtypes*) (equal (integer-type-to-fixtype (fixtype-to-integer-type fixtype)) fixtype)))