A top-level assert$-like command to ensure that a formula gets proved.
This takes the same arguments as thm. It wraps the thm into a must-succeed.
Macro: must-prove
(defmacro must-prove (&rest args) (cons 'must-succeed (cons (cons 'thm args) 'nil)))
