Some theorems about the built-in function set-difference$.
Theorem: true-listp-of-set-difference-equal
(defthm true-listp-of-set-difference-equal (true-listp (set-difference-equal x y)) :rule-classes (:rewrite :type-prescription))
