Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 19:24:22 -0800 (Mon, 09 Jan 2006)
Revision: 8438
Log message:

      Added the "simple" BTerm normalizer.  This didn't work as well
      as I had expected.  It cut the proof steps about 1/3, but I thought
      it would be more.  intro_term_TyAll is now about 100k primitive
      steps.
      
      Adding a fallback to the general form doesn't currently work,
      need to investigate.
      
      If you want to try using the original rule, in Itt_hoas_bterm_wf
      change normalizeBTermSimpleC to normalizeBTermForceC.