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.