Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-11 13:48:17 -0800 (Sun, 11 Dec 2005)
Revision: 8274
Log message:

      Sequent reduction is finished.  I don't know if there are any
      lessons here.  If anything I would say that, when performing
      rewriting under a binder, concentrate on defining closed terms that
      are equivalent to the destructors under the binder.  That's pretty
      obvious though.