Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-26 22:35:19 -0800 (Fri, 26 Dec 2003)
Revision: 5217
Log message:

      Ext_equal: standard dest_ext_equal and other standard functions added.
      
      Subtype: Elim-style lemmas to prove that subterms are types.
      
      Struct3: replaceWithHypT, replaceWithRevHypT replace "x:T" with "x:S" when "T =e S" in hyps.
      

Changes  Path
+7 -0 metaprl/theories/itt/itt_ext_equal.ml
+8 -4 metaprl/theories/itt/itt_ext_equal.mli
+8 -0 metaprl/theories/itt/itt_struct3.ml
+2 -0 metaprl/theories/itt/itt_struct3.mli
+4 -0 metaprl/theories/itt/itt_subtype.ml
+2130 -2144 metaprl/theories/itt/itt_subtype.prla