Tweak the way the E-Freeze-Final rule is written.

I'm actually writing out the callback function instead of just putting
`v`.  This is actually useful for the permutability proof; I think it
also makes the rule easier to understand.