Fixtype of statement values and errors.
This is a sum-of-products (i.e., union) type, introduced by fty::defflexsum.
Theorem: not-errorp-when-stmt-valuep
(defthm not-errorp-when-stmt-valuep (implies (stmt-valuep x) (not (errorp x))))