Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-24 22:20:53 -0800 (Wed, 24 Dec 2003)
Revision: 5215
Log message:

      Added two theorems(intro and elim style) about symmetry.
      Added two theorems that can replace equality in one type with equality in ext-equal type.
      May be last two rules should be added to elim-resource.
      

Changes	Path
+12 -0	metaprl/theories/itt/itt_ext_equal.ml
+715 -810	metaprl/theories/itt/itt_ext_equal.prla