Back to the email

Mathematically we would write this as all x: f.Pre(x) => f.Post(x)

Shouldn't it be all x: f.Pre(x) => f.Post(x, f(x))?