REVERSE using HONS instead of CONS
Function: hons-reverse
(defun hons-reverse (x) (declare (xargs :guard t)) (mbe :logic (reverse x) :exec (if (stringp x) (reverse x) (hons-revappend x nil))))
