`(q-compose-list xs l)` composes each UBDD in

**Function: **

(defun q-compose-list (xs l) (declare (xargs :guard t)) (if (atom xs) nil (cons (q-compose (car xs) l) (q-compose-list (cdr xs) l))))

**Theorem: **

(defthm q-compose-list-when-not-consp (implies (not (consp xs)) (equal (q-compose-list xs l) nil)))

**Theorem: **

(defthm q-compose-list-of-cons (equal (q-compose-list (cons x xs) l) (cons (q-compose x l) (q-compose-list xs l))))

**Theorem: **

(defthm ubdd-listp-of-q-compose-list (implies (and (force (ubdd-listp xs)) (force (ubdd-listp l))) (equal (ubdd-listp (q-compose-list xs l)) t)))