Uncurried primitives and simplified weak bisimilarity

- As Jeremy Yallop suggested, I change the semantics of the primitives
pair, proj1, proj2, fork, ret to offer them as base primitives. This
change has been filtered through to proofs and the extracted code. The
extracted code was then evaluated and surprisingly it worked on the
first run. The lack of currying actually reduced the number of errors
made by the extraction plugin.

- I have simiplified the weak bisimilarity based on the remark in
Sangiorgi's comment in his " The problem of “Weak Bisimulation up to” "
paper: I have proven that the single step based weak bisimilarity is
equivalent to the original and then went on to prove the monadic
properties, part of fork commutativity (only side effects, not the
switch yet) in 70 lines. This reduced the proof substantially as I did
not have to build my own inversion Lemmas, and push lemmas and I could
just use the built in ones. (To put it in perspective, it used to be
about 3000 lines long).