Reorganizing the process calculus examples

* Added the stuff from the bisimulation up to paper
Allow more tactics to consume hypotheses

The following forms are added:

  apply *H to ...
  apply ... to ... *H ...
  cut *H ...
  cut ... with *H
  inst *H with ...
  monotone *H with ...

In each case, if H names a hypothesis, then the tactic
consumes the hypothesis (like the clear tactic).

If H names a lemma, then the star has no effect.

When applying to unknowns, the unknowns may not be
starred. This follows the design that only explicitly
named things in a tactic are ever consumed.

Note that if hypothesis hints are given, then these
hints are used *after* consuming the hypotheses. Thus,
if one writes:

   foo : apply lem to *foo bar baz.

then the hypothesis named foo is effectively *replaced*
with a new hypothesis named foo that is the result of
applying the lem to the old foo and the other arguments.

The case tactic remains the only one that consumes the
hypothesis by default, so the (keep) annotation is
retained for it. This may be revisited in the future,
but it turns out not to be a conservative change.