Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 17:27:26 -0800 (Sat, 26 Nov 2005)
Revision: 8224
Log message:

      Proved basic theorems for vector lists.
      
      For now, the lists are dependent.  So, for example,
         vlist{| x: 1; y: 'x +@ 1 |} <--> vlist{| 1; 2 |}
      
      The dependencies produce complications, as you might
      imagine.  However, there doesn't seem to be any payoff
      in coding "nondependent" lists by substituting a constant
      (like it) for the hyp vars, so I'll stick with this for now.
      
      Likely, for real non-dependent lists, we would need contexts
      with no self-dependencies.  This might not help all that much
      either.
      
      Note that dependent values can be extremely useful in general,
      especially for coding things like mutually recursive functions
      and mutually recursive types.