Alternative proof style suggestion

[fabian-hk]

This is a suggestion to discuss an alternative proof style that only needs one match per function instead of a match for every called function that returns traceful or option.

[cwaldm]

I like the idea of removing the many matches!
It works well for the small examples (Two-message and Online).
However, it doesn't work right away for NSL. I currently don't fully understand why not. I pushed the broken version of NSL (containing admits).
If we figure out, how to resolve those, we can switch to this new style.
But for now, I would keep the current version.

[TWal]

I have been experimenting with this proof style in the past, the problem is that if a function in the middle fails (say, get_state), we must still prove that every function called before preserve the trace invariant.
In other words, if the function we are proving fail, this doesn't automatically proves the theorem, hence we cannot just deal with the success case.

I also dislike having nested matches, but I haven't found a better way yet.