		Search-engine friendly clone of the ACL2 documentation.

Add-to-set-equal-theorems

Some theorems about the built-in function add-to-set.

Definitions and Theorems

Theorem: true-listp-of-add-to-set-equal

(defthm true-listp-of-add-to-set-equal
  (equal (true-listp (add-to-set-equal a x))
         (true-listp x)))

Theorem: true-listp-of-add-to-set-equal-type

(defthm true-listp-of-add-to-set-equal-type
  (implies (true-listp x)
           (true-listp (add-to-set-equal a x)))
  :rule-classes :type-prescription)