Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-04 09:29:25 -0800 (Sun, 04 Dec 2005)
Revision: 8264
Log message:

      Added a theory of "sloppy" or "lazy" lists.  The intent is
      to minimize wf reasoning.
      
      The type Cons{n} stands for a term with at least 'n cons cells.
      It is defined with the Img type.
      
      Proved the key lemma
      
         l IN Cons{n} -->
         0 <= i < n -->
         l ~ (nth_prefix{l; i} @ nth_suffix{l; i})
      
      I used pairwise extensively.