Errata

Page 36, near bottom: ``the above predicate" - not immediately clear it refers to the $\exists BuyVieri$ predicate. Vieri being in the squad is logically equivalent to the current state being one right after buying him, though.

On page 45, the title of the book by Woodcock and Davies should refer to Proof after Refinement.