Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-25 09:57:47 -0800 (Wed, 25 Jan 2006)
Revision: 8604
Log message:

      Reflected rule definitions can use the usual meta-type checking
      mechanism Term_grammar.parse_rule.
      
      With sequent judgments, we have goals like the following
      
         bind{n; x. sequent_bterm{vsequent{| <J[x]> >- C[x] |}}} in BTerm
      
      Options:
         1. We can augment the normalizer with theorems for
            pushing binds through sequent_bterm, vsequent.
      
            One potential drawback is that we have assumed
            in many places that sequents are closed.
      
         2. We could define theorems for sequent_bterm{vsequent{| ... |}}
            in non-normal form.
      
      I think option 1 is probably better.
      
      The key theorem is as follows:
      
         bind{n; x. sequent_bterm{vsequent{| <J[x]> >- C[x] |}}}
         <-->
         sequent_bterm{vsequent{| hyp_context{n; x. hyplist{| <J[x]> |}};
                                  >- bind{n; x. C[x]} |}}
      
      We would have to define the non-vector hyp_context{n; x. ...} term,
      and then prove a bunch of theorems about open sequents.