(4vs-and-list-dumb sexprs) reduction ands together all the sexprs in
This is dumb in that it doesn't do the simple optimizations of 4vs-and-list, but it has a nicer 4v-sexpr-vars theorem because of this.
(defun 4vs-and-list-dumb (sexprs) (declare (xargs :guard t)) (if (atom sexprs) *4vt-sexpr* (4vs-and-dumb (car sexprs) (4vs-and-list-dumb (cdr sexprs)))))
(defthm 4v-sexpr-eval-of-4vs-and-list-dumb (equal (4v-sexpr-eval (4vs-and-list-dumb sexprs) env) (4v-and-list (4v-sexpr-eval-list sexprs env))))
(defthm 4v-sexpr-vars-of-4vs-and-list-dumb (equal (4v-sexpr-vars (4vs-and-list-dumb x)) (4v-sexpr-vars-list x)))