(intersectp x y) checks whether X and Y have any common
Logically we just check whether the intersect of X and
Y is empty.
In the execution, we use a faster function that checks for any common
members and doesn't build any new sets.
Definitions and Theorems
(defun intersectp (x y)
(declare (xargs :guard (and (setp x) (setp y))))
(mbe :logic (not (empty (intersect x y)))
:exec (fast-intersectp x y)))