Same as ex-from-rp when term is rp-termp but a little faster.
(ex-from-rp-loose term) → *
Function:
(defun ex-from-rp-loose (term) (declare (xargs :guard t)) (let ((__function__ 'ex-from-rp-loose)) (declare (ignorable __function__)) (mbe :logic (if (is-rp-loose term) (ex-from-rp-loose (caddr term)) term) :exec (case-match term (('rp & x) (ex-from-rp-loose x)) (& term)))))