(in-package "ACL2")

(include-book "app")

(defun rev (x)
  (if (endp x)
      x
    (app (rev (cdr x)) (list (car x)))))

(defthm rev-of-app
  (equal (REV (APP x y))
         (if (consp x)
             (app (rev y) (rev x))
           (rev y)))
  :hints (("Goal" :in-theory (enable app )))
  )

(defthm rev-rev
  (implies (true-listp x)
           (equal (rev (rev x))
                  x))
  :hints (("Goal" :do-not '(generalize eliminate-destructors))))