Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-17 12:29:52 -0700 (Tue, 17 May 2005)
Revision: 7290
Log message:

      Proved a theorem in itt_hoas_vector.
      But this proof depends on the theorem /itt/itt_fun2/fun_sqeq_intro
      I don't know how to prove this theorem. Is it true?
      

Changes	Path
+8 -0	metaprl/theories/itt/itt_fun2.ml
+896 -474	metaprl/theories/itt/itt_fun2.prla
+1 -0	metaprl/theories/itt/itt_hoas_vector.ml
+486 -320	metaprl/theories/itt/itt_hoas_vector.prla