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