Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-28 11:09:57 -0800 (Mon, 28 Nov 2005)
Revision: 8233
Log message:

      Proved the final wf goal.
      
         [wf] std_sequent{| <H> >- C |} in StdSequent{0} -->
         bsequent{| <H> >- C |} in Sequent
      
      Sequent is the "ugly" sequent triple (BTerm * BTerm list * BTerm),
      where the depths are increasing.
      
      The wf subgoal is unfortunate, but it may be the best we can do.
      What we really want to say is that all the terms in the sequent
      are "closed" wrt their dependencies, but this is impossible.
      
      So this approach is to prove that the std-style sequent is
      well-formed.  There are lemmas for many of the cases.