Allow Resume to be rerun without error

[xrchz]

If you redo the proof of a suspension, things don't work. You should be able to rerun the proof of a suspension even if you ran it already, without having to rerun the original suspension producer.

[mn200]

I think this will preclude reuse of suspension names. Currently, it's possible to write

Theorem foo: Phi 
Proof
  ... >> suspend "blah"
QED

and to then call suspend "blah" inside the resumption of blah. If you want the desired behaviour, the system will have to forbid this.

I don't at all think this is a problem btw.

[xrchz]

Yeah I'm happy to make that trade (rerun allowed in exchange for label reuse disallowed)