Use `return` instead of `result`

[nrc]

This would avoid shadowing any arguments called result. Would require mangling the name return in the predicate before injecting it into an assertion. Should also check that it is only used in postconditions.