Major Section: ACL2-BUILT-INS
The Common Lisp language allows its pairlis function to construct an alist in any order! So we have to define our own version: See pairlis$.
pairlis
