REVAPPEND

concatentate the reverse of one list to another 
Major Section:  PROGRAMMING

(Revappend x y) concatenates the reverse of the list x to y, which is also typically a list.

The following theorem characterizes this English description. 

(equal (revappend x y)
       (append (reverse x) y))
Hint: This lemma follows immediately from the definition of reverse and the following lemma. 
(defthm revappend-append
  (equal (append (revappend x y) z)
         (revappend x (append y z))))

The guard for (revappend x y) requires that x is a true list.

Revappend is defined in Common Lisp. See any Common Lisp documentation for more information.