Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-15 23:17:32 -0800 (Wed, 15 Mar 2006)
Revision: 8907
Log message:

      Some improvement; made the elimination rule proof a little more general.