Ray Richards noticed that there are several different definitions of
firstn in the distributed books:
ACL2 will thus complain if you try to include two or more of the above books.
You can fix the problem by modifying the definition of
each of these books to be as follows:
(defun firstn (n l)
"The sublist of L consisting of its first N elements."
(declare (xargs :guard (and (true-listp l)
(<= 0 n))))
(cond ((endp l) nil)
((zp n) nil)
(t (cons (car l)
(firstn (1- n) (cdr l))))))