Must-be-equal
Attach code for execution
The form (must-be-equal logic exec) evaluates to logic in
the ACL2 logic but evaluates to exec in raw Lisp. The point is to be
able to write one definition to reason about logically but another for
evaluation. Please see mbe and see mbt for appropriate macros
to use, rather than calling must-be-equal directly, since it is easy to
commute the arguments of must-be-equal by accident.
In essence, the guard for (must-be-equal x y) is (equal x y).
However, note that must-be-equal is a macro: (must-be-equal logic
exec) expands to (mbe1 exec logic), which expands to a call of return-last.
