> It is somewhat unfortunate both the proof obligation and proof 'declaration' use the same token.

There have been some RFCs open to improve this situation (e.g. unsafe blocks in unsafe functions comes to mind).