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

(defun rev (x)
  (if (consp x)
      (app (rev (cdr x))
           (list (car x)))
    nil))

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