Semantics fixes and half of associativity

Bug fixes in the semantics:
- Minor: The do bind rule had a bug where v >>= e would reduce to e' v
for some e', which obviously does not work
- Major: the move rules in for would only fire if both of the edges were
expressions, however this was breaking associativity

Overhaul in the way the fork commutativity is proved:
- Because of the above change many of the underlying lemmas had to be
changed, so I have changed the structure to be a little bit more
intuitive. Now there is some dead proof code, but I don't have a good
automatic way of identifying it.

Half of the associativity: I have essentially proven that fork a (fork b
c) simulates fork (fork a b) c. It is fairly involved so the other edge
will take time as well.

Adding LibTactics, the library used throughout the proofs.