Soundness issue: old as operator.

[MikaelMayer]

Consider the following code:

procedure f()
  modifies x, y
  ensures x == y ==> old(x) != old(y)
{
   if x != y {
      x := y;
   } else {
     x := y + 1;
   }
}

Unfortunately, we encode old() as an application of "old" operator to the argument.
Hence, it should be provable in lambda that x == y ==> old(x) == old(y), so the procedure above would theoretically able to prove false.

To fix this, we shouldn't use operator application to describe the old value of variables.