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)
  // ...