acl2 эквациональное рассуждение, доказывающее равенство

Question

Я пытаюсь доказать, что следующая функция верна, и у меня возникают проблемы с ее выяснением, хотя это кажется очевидным!

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

при этом мне просто нужно показать, что (app (rev x) (rev y)) эквивалентно (rev (app xy)))), используя функции:

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

Вот как я сделал еще один (надеюсь, правильно)

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

"обратное добавление"

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

(len (rev (cons x y))

= def of rev

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

= выходной контракт оборотов

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

= "обратное добавление"

(len (rev (cons x y))

= выходной контракт оборотов

(len (cons x y))

= лен

(+ 1 (len y))

= выходной контракт оборотов

(+ 1 (len (rev y)))