Started the fork proofs. 
- I have defined the function swapf which essentially swaps the end
result of a fork. This is important because one cannot prove 

fork a b = fork b a 

directly (they return different things). Either one assumes something
silly like (a,b) = (b,a) or proves

fork a b = (fork b a >>= swap)

which is true. I went on to prove that swap does in deed swap (i.e.:
given a pair it is weakly bisimilar to the the swapped version). 

This meant I had to prove a number of properties about the reduction
relation (mostly things about deterministic tau reductions of
expressions).