Refer to precondition state from the postcondition

[nrc]

Example (from Reddit user thiez):

#[postcond = "self.x=\old(self.x)+1"]
fn inc(&mut self) {
    self.x += 1;
}

The /old function in this example allows us to speak about the old state of self.x.

Need to figure out the best syntax for this, perhaps allowing some variables to be introduced and filled with the old values. This probably needs to be opt-in since there will be a cost of the copy.