Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-24 18:21:06 -0800 (Sun, 24 Feb 2002)
Revision: 3515
Log message:

      Added definition for equivalence relations, which are more general
      than "equal" and are necessary in the context of groups.
      
      TODO:
         1. Might need to define functionality for equivalence relations
            and update the substitution rules.
         2. Implement equivalence class.
      

Changes	Path
Added	metaprl/theories/czf/czf_itt_equiv.ml
Properties	metaprl/theories/czf/czf_itt_equiv.ml
Added	metaprl/theories/czf/czf_itt_equiv.mli
Properties	metaprl/theories/czf/czf_itt_equiv.mli
Added	metaprl/theories/czf/czf_itt_equiv.prla
Properties	metaprl/theories/czf/czf_itt_equiv.prla