RASSOC

look up value in association list, using eql as test 
Major Section:  PROGRAMMING

(Rassoc x alist) is similar to (assoc x alist), the difference being that it looks for the first pair in the given alist whosew QUANTIFIERS-USING-DEFUN-SK-EXTENDED.html -- ACL2 Version 2.9

QUANTIFIERS-USING-DEFUN-SK-EXTENDED

quantification example with details 
Major Section:  QUANTIFIERS

See quantifiers-using-defun-sk for the context of this example. 

(in-package "ACL2")


; We prove that if every member A of each of two lists satisfies the
; predicate (P A), then this holds of their append; and, conversely.


; Here is a solution using explicit quantification.


(defstub p (x) t)


(defun-sk forall-p (x)
  (forall a (implies (member a x)
                     (p a)