introduce old outside of post condition

[samuelchassot]

It can be implemented a sugar instead of writing a snapshot at the beginning of the body:

def f() = 
  // mutable operations
  assert(old(this).size > this.size)
  // ...

would be transformed into

def f() = 
  @ghost val oldthis = snapshot(this)
  // mutable operations
  assert(oldThis.size > this.size)
  // ...

[vkuncak]

Be careful about semantics when using old in nested functions, as this could lead to some ambuguity if there is variable shadowing: did the user mean old as "at the entry of the inner function", as in "at the entry of outer function". The behavior of whether the variable is considered changed by a nested function has changed recently in #1532