PAIRLIS

See pairlis$
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$.