FR: add a way to assume that the current function satisfies no_unwind

[bsdinis]

no_unwind is required for types that have invariants (if a call that takes &mut self unwinds, it can break the type invariant).

This is a good thing, but it can become overly restrictive.
Any type that has exec containers (e.g., Vec, HashMap, BTreeMap) cannot insert to the values, because those calls may unwind.

It would be useful to admit that a particular function does not unwind. Unwinds are unlikely and it only affects correctness if the code has panic hooks (otherwise the panic just crashes the program). It would be useful to be able to admit it and continue with the proof