Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 13:03:50 -0800 (Sat, 26 Nov 2005)
Revision: 8221
Log message:

      Added the initial vector-list theory.
      Unfortunately, it looks like I'm hitting a rewriter bug.
      See Itt_vec_list1.reduce_vlist_cons for an example.
      
      Here is the failing fragment.
      
         happly{hlambda{'e; x. sequent_ind{... Sequent{ <J['x]> >- ... }}; 'e}
         --> sequent_ind{... Sequent{ <J['x]> >- ... }}
      
      In other words, the 'x in <J['x]> is not getting substituted.
      The two "x"s *should* be the same variable.