Theorem about the static soundness of literal execution.
This is very simple, because both static and dynamic semantics evaluate the literal.
We also show that it returns one value.
Theorem:
(defthm exec-literal-when-check-safe-literal (implies (not (reserrp (check-safe-literal lit))) (b* ((outcome (exec-literal lit cstate))) (and (not (reserrp outcome)) (equal (eoutcome->cstate outcome) (cstate-fix cstate)) (equal (len (eoutcome->values outcome)) 1)))))