is it allowed to access locals in a postcondition? I don't think it makes much sense...
If we have a closure in the postcondition we get warnings about using the same variable names:
is this what we want?
I don't know. I am of two minds here.
Obviously when I coded that I did not think of postconditions. On the other hand, even if this is forbidden maybe the local's scope is too "near"?