[Feature request]: Name assertions in functions

[MikaelMayer]

What is the feature you would like to see in a future version of Dafny?

I would like to prove, name and hide assertions in functions like in methods.

This works

But this doesn't

As a result, one cannot prove a result, hide it from the verifier, and reuse it later in the function, one has to either prove it again or make it available for every assertion, which is suboptimal.