Returns the first element of a non-empty list, else nil
Completion Axiom (completion-of-car):
(equal (car x) (cond ((consp x) (car x)) (t nil)))
Guard:
(or (consp x) (equal x nil))
Notice that in the ACL2 logic, car returns nil for every atom.
