(faig-const-list->4v-list x) → *
Function:
(defun faig-const-list->4v-list (x) (declare (xargs :guard t)) (let ((__function__ 'faig-const-list->4v-list)) (declare (ignorable __function__)) (if (atom x) nil (cons (faig-const->4v (car x)) (faig-const-list->4v-list (cdr x))))))
Theorem:
(defthm nth-of-faig-const-list->4v-list (4v-equiv (nth n (faig-const-list->4v-list args)) (faig-const->4v (nth n args))))