CAR

returns the first element of a non-empty list, else nil
Major Section:  PROGRAMMING

Completion Axiom:

(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.