(value-map-fix x) is a usual ACL2::fty omap fixing function.
(value-map-fix x) → *
Theorem:
(defthm value-mapp-of-value-map-fix (value-mapp (value-map-fix x)))
Theorem:
(defthm value-map-fix-when-value-mapp (implies (value-mapp x) (equal (value-map-fix x) x)))
Theorem:
(defthm emptyp-value-map-fix (implies (or (omap::emptyp x) (not (value-mapp x))) (omap::emptyp (value-map-fix x))))
Theorem:
(defthm emptyp-of-value-map-fix-to-not-value-map-or-emptyp (equal (omap::emptyp (value-map-fix x)) (or (not (value-mapp x)) (omap::emptyp x))))