Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-29 17:41:26 -0800 (Sun, 29 Jan 2006)
Revision: 8621
Log message:

      Initial progress toward append-style sequents and binders.
      
      This initial naive definition is not satisfactory.
      
      Here is the problem.  The append-binder has the following rule:
      
         mk_flat_vbind{| x: A; <J[x]> >- e[x] |} <-->
            mk_bind{length{A}; x. mk_flat_vbind{| <J[x]> >- e[x] |}}
      
      This means that it is possible to define some strange terms.
      
         mk_flat_bind{| x: A; y: append{x; x} >- e[x; y] |}
      
      This says that the "y" binder has twice as many bindings
      as the "x" binder.  This is clearly bogus.
      
      I'm not sure exactly how to fix it.  We could require non-self-bindings
      in the context, but that is probably too strong.
      
      It seems like we would prefer a sequent_ind form that would allow
      the substitions for the hyps and concl to differ.
      
      Perhaps we can do two-phase, where the first phase squashes the terms
      in the context.  We'll see.