Very basic list lemmas for svexlist-eval.
Theorem:
(defthm svexlist-eval-when-atom-cheap (implies (atom x) (equal (svexlist-eval x env) nil)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm svexlist-eval-nil (equal (svexlist-eval nil env) nil))
Theorem:
(defthm car-of-svexlist-eval (4vec-equiv (car (svexlist-eval x env)) (svex-eval (car x) env)))
Theorem:
(defthm cdr-of-svexlist-eval (4veclist-equiv (cdr (svexlist-eval x env)) (svexlist-eval (cdr x) env)))
Theorem:
(defthm svexlist-eval-of-cons (equal (svexlist-eval (cons a b) env) (cons (svex-eval a env) (svexlist-eval b env))))
Theorem:
(defthm consp-of-svexlist-eval (equal (consp (svexlist-eval x env)) (consp x)))
Theorem:
(defthm svexlist-eval-under-iff (iff (svexlist-eval x env) (consp x)))
Theorem:
(defthm len-of-svexlist-eval (equal (len (svexlist-eval x env)) (len x)))
Theorem:
(defthm svexlist-eval-of-append (equal (svexlist-eval (append a b) env) (append (svexlist-eval a env) (svexlist-eval b env))))
Theorem:
(defthm svex-eval-of-nth (4vec-equiv (nth n (svexlist-eval x env)) (svex-eval (nth n x) env)))
Theorem:
(defthm nthcdr-of-svexlist-eval (equal (nthcdr n (svexlist-eval x env)) (svexlist-eval (nthcdr n x) env)))