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

(defun rev (x)
  (if (endp x)
    nil
    (app (rev (cdr x)) (cons (car x) nil))))

#| <- uncomment these to prove rev-app
(defthm app-type
  (implies (true-listp y)
           (true-listp (app x y)))
  :rule-classes (:rewrite :type-prescription))

(defthm rev-type
  (true-listp (rev x))
  :rule-classes (:rewrite :type-prescription))
;|#

(defthm rev-app
  (equal (rev (app x y))
         (app (rev y) (rev x))))