Lposfix
(lposfix x) is logically identical to (pos-fix x), but its
guard requires that x is a posp and, in the execution, it's just a
no-op that returns x.
Definitions and Theorems
Function: lposfix$inline
(defun lposfix$inline (x)
(declare (xargs :guard (posp x)))
(mbe :logic (pos-fix x) :exec x))
