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