Added three files:
- weakBisimulations.v
   * Defines silent reductions
   * Defines deterministic silent reductions (i.e.: silent reductions
that has to be taken) (proof: deterministic silent reduction is silent)
   * Defines the weak labelled reduction (i.e.: 0 or more silent
reductions followed by a labelled reduction followed by 0 or more silent
reductions, (t)* (l) (t)*.
   * Defines the weak simulation relation (proofs: reflexive,
transitive)
   * Defines the weak bisimilarity relation (proofs: reflexive,
transitive, symmetric) 
   * Silent reduction from a to b implies that b weakly simulates a.
   * If there is a deterministic silent reduction from a to b and there
is a silent reduction from a to c, then either there is a deterministic
silent reduction from a to c and then from c to b or there is a silent
reduction from b to c. 
   * If there is a deterministic silent reduction from a to b then a and
b are weakly bisimilar.
- mconbaseMonProofs.v 
  * This has the content that originally came from mcontests.v, that is
    # Monadic left identity beta reduces
    # Monadic right identity beta reduces
    # Monadic associativity beta reduces to the same thing
  * Added the (corrected) proofs from mconequivproofs.v (they really
didn't belong there)
    # If a term reduces it is not a value
    # The value relation is decideable
    # A variable cannot be typed in an empty environment
  * Added proofs of deterministic silent reductions to make bisimilarity
proofs easier
    # JO_red_ret
    # JO_red_evalbind
    # JO_red_dobind
    # JO_red_app
  * Proofs of bisimilarity. Note, these are _much_ stronger statements
than the previous beta reduction ones though they take similar forms.
    # Monadic left identity, that is "ret a >>= fun x. e" is equivalent
to "(fun x. e) a"
    # Monadic right identity, "live a >>= ret" is equivalent to "live a"
    # Monadic associativity, that is "(live a >>= fun x. e) >>= fun y.
e'" is equivalent to "live a >>= fun z. ((fun x. e) z >>= fun x. e)".
- mconequivproofs.v 
  * Fixed the value relation proof.
  * Removed the unneccessary proofs mentioned above.