		Search-engine friendly clone of the ACL2 documentation.

Std/system/all-vars

Theorems about all-vars.

See the file for lemmas about all-vars1.

Theorem: symbol-listp-of-all-vars

(defthm symbol-listp-of-all-vars
  (implies (pseudo-termp term)
           (symbol-listp (all-vars term))))

Theorem: true-listp-of-all-vars

(defthm true-listp-of-all-vars
  (true-listp (all-vars term))
  :rule-classes (:rewrite :type-prescription))