ASSOC-EQ
look up key in association list, using eq as test
Major Section: PROGRAMMING
(Assoc-eq x alist) is the first member of alist whose car
is x, or nil if no such member exists.
(Assoc-eq x alist) is provably the same in the ACL2 logic as
(assoc x alist) and (assoc-equal x alist), but it has a
stronger guard because it uses eq for a more efficient test for
whether x is equal to a given key of alist. Its guard
requires that alist is an association list (see alistp), and
moreover, either x is a symbol or all keys of alist are
symbols, i.e., alist is a symbol-alistp.
