Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-23 23:22:12 -0800 (Sat, 23 Mar 2002)
Revision: 3543
Log message:

        Added and proved the rule for the property "if a is equivalent to b
        under any equivalence relation, then a is equal to b". It is proved
        by the use of "set builder" defined in Czf_itt_set_bvd.
      

Changes	Path
+17 -12	metaprl/theories/czf/czf_itt_equiv.ml
+5553 -4023	metaprl/theories/czf/czf_itt_equiv.prla