Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-26 13:53:20 -0800 (Mon, 26 Dec 2005)
Revision: 8367
Log message:

      Working on a list_of_fun theory.
      
      The main problem with list_of_fun{i. 'f['i]; 'n} is that
      the function 'f['i] can be arbitrary, and reasoning about
      arbitrary functions is hard.
      
      In particular, information can be lost during normalization.
      For example:
      
          interactive_rw nth_prefix_lof {| normalize_lof |} :
             'n in nat -->
             'm in nat -->
             'm <= 'n -->
             nth_prefix{lof{i. 'f['i]; 'n}; 'm}
             <-->
             lof{i. 'f['i]; 'm}
      
      Here, we lost some information (the variable 'n), and so the rewrite is
      not easy to reverse.
      
      The plan is to define a set of reversible rewrites for lof normalization.