set-defuns

(defun adjoin-equal
  (x l)
  (declare (xargs :guard (true-listp l)))
  (if (member-equal x l)
    l
    (cons x l)))

(defun memberp-equal
  (x l)
  (declare (xargs :guard (true-listp l)))
  (consp (member-equal x l)))

(defun set-equal
  (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (and (subsetp-equal a b) (subsetp-equal b a)))

(defun setp-equal
  (l)
  (declare (xargs :verify-guards t))
  (and (true-listp l) (no-duplicatesp-equal l)))