Major Section: PROGRAMMING Append, which takes two or more
arguments, expects all the arguments except perhaps the last to
be true (null-terminated) lists. It returns the result of
concatenating all the elements of all the given lists into a
single list. Actually, in ACL2 is a macro that expands into
calls of the binary function Append is a Common Lisp function.
See any Common Lisp documentation for more information.