Look up key in a keyword-value-listp
If l is a list of even length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword, then (assoc-keyword key l) is the first tail of l starting with key if key is some ki, and is nil otherwise.
The guard for (assoc-keyword key l) is (keyword-value-listp l).
Function: assoc-keyword
(defun assoc-keyword (key l) (declare (xargs :guard (keyword-value-listp l))) (cond ((endp l) nil) ((eq key (car l)) l) (t (assoc-keyword key (cddr l)))))