rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def EquivRel x,y:T. E(x;y)
Def == Refl(T;x,y.E(x;y)) & (Sym x,y:T. E(x;y)) & (Trans x,y:T. E(x;y))

is mentioned by

Thm* E:(TTProp). (EquivRel x,y:T. E(x,y))  (EquivRel x,y:T. E(x,y))[squash_thru_equiv_rel]
Thm* R:(TTProp). 
Thm* (EquivRel x,y:T. R(x,y))
Thm* 
Thm* (a,a',b,b':T. R(a,b)  R(a',b')  (R(a,a')  R(b,b')))		[equiv_rel_self_functionality]
Thm* E:(TTProp), E':(T'T'Prop).
Thm* T = T'
Thm* 
Thm* (x,y:T. E(x,y)  E'(x,y))
Thm* 
Thm* ((EquivRel x,y:T. E(x,y))  (EquivRel x,y:T'. E'(x,y)))		[equiv_rel_functionality_wrt_iff]
Thm* EquivRel A,B:Prop. A  B[equiv_rel_iff]
Thm* R:(TTProp). 
Thm* Preorder(T;x,y.R(x,y))  (EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b))		[symmetrized_preorder]
Thm* R:(TTType), Q:(TProp).
Thm* (EquivRel x,y:T. R(x,y))  (EquivRel x,y:{z:T| Q(z) }. R(x,y))		[equiv_rel_subtyping]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

rel 1 Sections StandardLIB Doc