Extension of 4v-<= to four-valued lists.

We say X <= Y for four-valued lists when:

- Y is at least as long as X, and
- Xi <= Yi for all i up to |X|.

**Function: **

(defun 4v-list-<= (x y) (declare (xargs :guard t)) (if (atom x) t (and (consp y) (4v-<= (car x) (car y)) (4v-list-<= (cdr x) (cdr y)))))

**Theorem: **

(defthm 4v-list-<=-nth (implies (4v-list-<= a b) (4v-<= (nth n a) (nth n b))))