Returns the second element of a cons pair, else nil
Completion Axiom (completion-of-cdr):
(equal (cdr x) (cond ((consp x) (cdr x)) (t nil)))
Guard:
(or (consp x) (equal x nil))
Notice that in the ACL2 logic, cdr returns nil for every atom.
