concatenate two strings
Major Section:  ACL2-BUILT-INS

String-append takes two arguments, which are both strings (if the guard is to be met), and returns a string obtained by concatenating together the characters in the first string followed by those in the second. Also see concatenate, noting that the macro call

(concatenate 'string str1 str2).
expands to the call
(string-append str1 str2).

To see the ACL2 definition of this function, see pf.