(defmacro app (&rest rst) `(append ,@rst))
(add-macro-fn app binay-append) 
(defmacro tlp (l) `(acl2::true-listp ,l))
(add-macro-fn tlp true-listp) 

(defun-sk E-Fz (u v)
  (exists z (equal (app u v) (rev z))))

#|

 This generates the following events, where e-fz-witness is a new
 function symbol, a Skolem function. 

 (defun-nx e-fz (u v)
   (let ((z (e-fz-witness u v)))
        (equal (app u v) (rev z))))

 Since we can't say exist a function s.t. ... in FO, we instead say
 that if

 (app u v) = (rev z) for any z, then (app u v) = (rev (e-fz-witness u v))

 So, we add the following constraint so that e-fz-witness is not just
 any function, but one restricted by e-fz-suff.

 (defthm e-fz-suff
   (implies (equal (app u v) (rev z))
            (e-fz u v)))

 Now, we can use ACL2s to reason about quantifiers. Typically, we do
 this by defining a function that provides the z above. Here is an
 example.

|#

:pe e-fz
:pf e-fz
:pe e-fz-suff
:pcb! :x

(defunc fz (u v) ; define a function that generates a witness
  :input-contract (and (tlp u) (tlp v))
  :output-contract (tlp (fz u v))
  (app (rev v) (rev u)))

(defthm fz-thm ; show that fz works
  (implies (and (tlp u) (tlp v))
           (equal (rev (fz u v))
                  (app u v))))

(in-theory (disable fz-definition-rule))

(defthm existential-reasoning-example ; prove an existential
  (implies (and (tlp u) (tlp v))
           (e-fz u v))
  :hints (("goal" :use fz-thm
           :in-theory (disable fz-thm))))