Theorems about flatten-ands-in-lit.
Theorem: pseudo-term-listp-of-flatten-ands-in-lit
(defthm pseudo-term-listp-of-flatten-ands-in-lit (implies (pseudo-termp term) (pseudo-term-listp (flatten-ands-in-lit term))))