Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-09 15:24:41 -0800 (Fri, 09 Dec 2005)
Revision: 8271
Log message:

      This time I think I really have it solved--but we'll see.  The problem
      with all the different approaches is that the conversion expression
      includes a destructor, which is in general in the scope of binders.
      However, the destructor doesn't care about the binders, so the computation
      should work anyway.
      
      In general, the issue is that we need to solve the following rewrite,
      for <K> nonempty.  Note that <K> *does* depend on <J>, however the
      length{...} doesn't care.
      
         (<J> >-bind if length{hypconslist{| <K> >- nil |}} then nil else e2)
         <-->
         (<J> >-bind e2)
      
      The idea is pretty simple.  All I've proved so far
      is the unconditional rewrite
      
         length{hypconslist{| <K> >- nil |}}
         <-->
         length{squashlist{| <K> >- nil |}}
      
      where squashlist{| ... |} evaluates to a real list
         [it; ...; it]
      
      This *should* be enough, because rewriting with
      squashlist{| ... |} is easy because the bindings
      go away.