Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-05 02:32:33 -0800 (Sat, 05 Feb 2005)
Revision: 6601
Log message:

      added and proved some useful rules.
      
      Alexei, can you take a look at "all_list_elim"? It seems that we have to add sth about the wellformedness of 'P.
      

Changes	Path
+46 -13	metaprl/theories/itt/itt_list2.ml
+4596 -3141	metaprl/theories/itt/itt_list2.prla