acl2 equational reasoning, proving equality

Question

I'm trying to prove the following function true and am having trouble figuring it out, even though it seems so obvious!

(implies (and (listp x)
              (listp y))
         (equal (app (rev x) (rev y))
                (rev (app x y))))

by doing so i just need to show that (app (rev x) (rev y)) is equivalent to (rev (app x y)))), using the functions:

(defunc len (x)
  :input-contract t
  :output-contract (natp (len x))
  (if (atom x)
    0
    (+ 1 (len (rest x)))))

(defunc atom (x)
  :input-contract t
  :output-contract (booleanp (atom x))
  (not (consp a)))

(defunc not (a)
  :input-contract (booleanp a)
  :output-contract (booleanp (not a))
  (if a nil t))

(defunc listp (l)
  :input-contract t
  :output-contract (booleanp (listp l))
  (or (equal l ())
      (consp l)))

(defunc endp (a)
  :input-contract (listp a)
  :output-contract (booleanp (endp a))
  (not (consp a)))

(defunc twice (l)
  :input-contract (listp l)
  :output-contract (listp (twice l))
  (if (endp l)
    nil
    (cons (first l) (cons (first l) (twice (rest l))))))

(defunc app (a b)
  :input-contract (and (listp a) (listp b))
  :output-contract (listp (app a b))
  (if (endp a)
    b
    (cons (first a) (app (rest a) b))))

(defunc rev (x)
  :input-contract (listp x)
  :output-contract (and (listp (rev x)) (equal (len x) (len (rev x))))
  (if (endp x)
    nil
    (app (rev (rest x)) (list (first x)))))

this is how i did another one (hopefully correctly)

(implies (listp y)
         (equal (len (rev (cons x y)))
                (+ 1 (len (rev y)))))

"reverse append thing"

(rev (app (rev y) (rex x))) = (app x y)

(len (rev (cons x y))

= def of rev

len (app (rev y) (list x))

= output contract of rev

(len (rev (app (rev y) (list x))))

= "reverse append thing"

(len (rev (cons x y))

= output contract of rev

(len (cons x y))

= def of len

(+ 1 (len y))

= output contract of rev

(+ 1 (len (rev y)))