BINARY-APPEND

concatenate two lists 
Major Section:  PROGRAMMING

This binary function implements append, which is a macro in ACL2. See append

The guard for binary-append requires the first argument to be a true-listp.