Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:28:45 -0800 (Mon, 01 Apr 2002)
Revision: 3552
Log message:

      Removed the introduction rule for "equiv" since it made proofs awkard
      and could be easily substitued with a rewrite rule;
      Reproved related rules.
      

Changes	Path
+0 -9	metaprl/theories/czf/czf_itt_equiv.ml
+4252 -3300	metaprl/theories/czf/czf_itt_equiv.prla