Substitute is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot
take keyword arguments (though macros can), the test used in
substitute is eql.
eql as test
Major Section: PROGRAMMING
(Substitute new old seq) is the result of replacing each occurrence
of old in seq, which is a list or a string, with new.
The guard for substitute requires that either seq is a string and
new is a character, or else: seq is a true-listp such that either
all of its members are eqlablep or old is eqlablep.
Substitute is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot
take keyword arguments (though macros can), the test used in
substitute is eql.