Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-22 21:16:48 -0800 (Sun, 22 Jan 2006)
Revision: 8570
Log message:

      [Ping Aleksey]  Take a look at the following address:
            /itt_reflection_experimental/itt_hoas_relax1/vbind_eta_expand/1/1/1/1/1/1
         At this location, reduceC does something different than
         (sweepDnC reduceC), in fact reduceC does not work.  This might
         be a coding error In Itt_hoas_vbind.squash_vbind_conv, but I don't
         think so.  It seems that squash_vbind_conv either succeeds or raises
         RefineError, and if it succeeds, it makes progress.  So it would
         seem that reduceC should apply to all terms, but it does not.
      
      Mostly proved the forward chaining wf rules for BSequent.
      They will need to be changed a bit.
      
      Added vector binders to Itt_hoas_relax1.