Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-19 12:37:18 -0800 (Mon, 19 Dec 2005)
Revision: 8321
Log message:

      Here is a slightly different approach, where the idea
      is to rewrite
      
         substl{substl{'e; 'l1}; 'l2}
         <-->
         substl{'e; append{'l1; 'l2}}
      
      To do so, we need to know that 'l1 and 'l2 are lists.
      The Itt_hoas_vector.bindn_to_list_of_fun is such
      an attempt:
      
         bind{'n; x. 'e['x]}
         <-->
         bind{'n; x. 'e[list_of_fun{i. nth_elem{'x; 'i}; 'n}]}
      
      Unfinished, the proof is not easy AFAIK.