Mbt*
Introduce a guard proof obligation
The macro mbt* is a variant of mbt (``must be true'').
However, unlike mbt, the call (mbt* test) is equivalent simply to
t for both logic and evaluation. The only effective difference between
(mbt* test) and t is that (mbt* test) generates a guard
proof obligation (when used in a logic-mode definition) of
test.
If you think that mbt* might be of use, please see assert*,
which is defined using mbt* to create a guard proof obligation
without any logical or execution burden.
