Modification to make fork fair (and maybe slightly less complex)
Propagating changes. So far so painless.
Modified fork commutativity proof to work with the fair fork version.
A lemma used to make the fork proof slightly quicker: If A
deterministically and silently reduces to both B and C, then either B
deterministically, silently reduces to C or vice versa, corresponding to
the deterministic orders (ABC and ACB).
Merge pull request #11 from tk407/FairFork

Fair fork