Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 21:06:29 -0700 (Sun, 02 Apr 2006)
Revision: 9000
Log message:

      Added equalityElimination rule (which postulates that any witness for an
      equality is an "it") to AutoOK part of elim (instead of the AutoComplete part
      of it, where it used to be). I've also added an appropriate guard to it to
      make sure that it will only be used when it can actually make progress.
      
      P.S. This commit breaks three proofs in itt_hoas_bterm_wf; will fix those
      in a little while.