Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 08:15:28 -0800 (Wed, 30 Nov 2005)
Revision: 8246
Log message:

      Committing some half-completed work before we lose it.  The
      Itt_hoas_sequent_term1 sequent-coding converts a sequent to ugly form
      without any wf subgoals, using a bind-pushing trick similar to the one
      in Itt_hoas_debruijn.  The arguments have to be carefully constructed,
      it is about half done.