Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-15 21:29:33 -0800 (Sun, 15 Jan 2006)
Revision: 8487
Log message:

      Reproved the Itt_hoas_sequent_bterm1 using relaxed properties.
      Proved the forward-chaining rules.  My proofs should be cleaned
      up, I was too lazy.
      
      The forward rules have the following wf requirements
      
         hyps in CVarRelaxed{0}
         concl in Bind{length{hyps}}
      
      These goals are extremely easy to prove via theorems like
      Itt_hoas_relax.mk_bterm_in_bindn:
      
         "wf" : <H> >- n = m in nat -->
         "wf" : <H> >- subterms in list -->
         <H> >- mk_bterm{n; op; subterms} in Bind{m}
      
      They also hold, by construction, on all bsequent{| ... >- ... |}.
      
      Current state:
         - We need better tactics for membership in Bind.  It is often
           a mistake to use (x in BTerm => x in Bind), so there are a
           bunch of nth_hyp to control the application.  This is
           inefficient, and we get too many cases that are not covered.
      
         - Need to prove the properties for bsequent{| ... |}, and
           reprove the forward rules in Itt_hoas_sequent_term1.
           Note that these are the strong rules (the non-eta-expanded
           rules).