Extension of 4v-<= to four-valued lists.
We say X <= Y for four-valued lists when:
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))))