Built-in axioms and theorems about booleans.
Theorem:
(defthm booleanp-compound-recognizer (equal (booleanp x) (or (equal x t) (equal x nil))) :rule-classes :compound-recognizer)
Theorem:
(defthm boolean-listp-cons (equal (boolean-listp (cons x y)) (and (booleanp x) (boolean-listp y))))
Theorem:
(defthm boolean-listp-forward (implies (boolean-listp (cons a lst)) (and (booleanp a) (boolean-listp lst))) :rule-classes :forward-chaining)
Theorem:
(defthm boolean-listp-forward-to-symbol-listp (implies (boolean-listp x) (symbol-listp x)) :rule-classes :forward-chaining)