(set-verify-guards-eagerness 2) ; avoids some declare forms

(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
    y))

(defun rev-logic (x)
  (if (consp x)
      (app (rev-logic (cdr x)) (cons (car x) nil))
    nil))

(defun rev-exec (x acc)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      acc
    (rev-exec (cdr x)
              (cons (car x) acc))))

(defun rev (x) ; FAILS
  (declare (xargs :guard (true-listp x)))
  (mbe :logic
       (rev-logic x)
       :exec
       (rev-exec x nil)))

(defthm rev-logic-is-rev-exec
  (equal (rev-exec x y)
         (app (rev-logic x) y)))

(defun rev (x)
  (declare (xargs :guard (true-listp x)))
  (mbe :logic
       (rev-logic x)
       :exec
       (rev-exec x nil)))