4vs-or-list
(4vs-or-list x) reduction ors together all the sexprs in the list
x, producing a single sexpr representing their disjunction.
Definitions and Theorems
Function: 4vs-or-list
(defun 4vs-or-list (x)
(declare (xargs :guard t))
(if (atom x)
*4vf-sexpr*
(4vs-or (car x) (4vs-or-list (cdr x)))))
