(maybe-natp-fix x) is the identity for maybe-natps, or
coerces any invalid object to
Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.
(defun maybe-natp-fix$inline (x) (declare (xargs :guard (maybe-natp x))) (mbe :logic (if x (nfix x) nil) :exec x))
(defthm maybe-natp-of-maybe-natp-fix (maybe-natp (maybe-natp-fix x)) :rule-classes (:rewrite :type-prescription))
(defthm maybe-natp-fix-when-maybe-natp (implies (maybe-natp x) (equal (maybe-natp-fix x) x)))
(defthm maybe-natp-fix-under-iff (iff (maybe-natp-fix x) x))
(defthm maybe-natp-fix-under-nat-equiv (nat-equiv (maybe-natp-fix x) x))