The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E.
[1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
[1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.