(lifix x) is logically identical to
(lifix x) is an inlined, enabled function that just expands into
(mbe :logic (ifix x) :exec x)
To understand why you might want this, see the analogous discussion about lnfix.
(defun lifix$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (ifix x) :exec x))