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