(in-package "ACL2")

(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))

; Fails:
#||
(defthm rev-app
  (equal (rev (app x y))
         (app (rev y) (rev x))))
||#

; Checkpoint:

#||
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV Y) (APP (REV Y) NIL)))
||#

(local
 (defthm app-nil
   (implies (true-listp x)
            (equal (app x nil)
                   x))))

(local
 (defthm true-listp-rev
   (true-listp (rev x)))) ; OR: (equal (true-listp (rev x)) t)

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

; Now to be fancy, exploiting deep knowledge of ACL2's "type inference"
; mechanism (and definitely not necessary!).

#||

(ubt! 2)

(defthm true-listp-app
  (implies (true-listp y)
           (true-listp (app x y)))
  :rule-classes :type-prescription)

(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))))
||#