Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-15 01:14:09 -0800 (Sun, 15 Jan 2006)
Revision: 8483
Log message:

      Added elimination rules which do not do thinning. The one with bindings is hard; not proved yet.