Major Section: ACL2-BUILT-INS
(strip-cdrs x) has a guard of (alistp x), and returns the list
obtained by walking through the list x and collecting up all second
components (cdrs). This function is implemented in a tail-recursive
way, despite its logical definition.
To see the ACL2 definition of this function, see pf.
