Does a 4v-sexpr always evaluate to a purely Boolean value, i.e., is it never X or Z?
(4v-sexpr-purebool-p sexpr) is a logically nice, but non-executable way to express pure Boolean-ness. See also 4v-sexpr-purebool-check, which can be executed, and uses a SAT solver to answer the question.
(defthm 4v-sexpr-purebool-p-necc (implies (not (or (equal (4v-sexpr-eval sexpr env) (4vt)) (equal (4v-sexpr-eval sexpr env) (4vf)))) (not (4v-sexpr-purebool-p sexpr))))
(defthm 4v-sexpr-purebool-p-to-faig-purebool-p (equal (4v-sexpr-purebool-p sexpr) (faig-purebool-p (sfaig sexpr))))