num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm* a,b,a',b':. (a ~ a' (b ~ b' ((a ~ b (a' ~ b'))[assoced_functionality_wrt_assoced]
cites the following:
0Thm* R:(TTProp). 
Thm* (EquivRel x,y:TR(x,y))
Thm* 
Thm* (a,a',b,b':TR(a,b R(a',b' (R(a,a' R(b,b')))
[equiv_rel_self_functionality]
2Thm* EquivRel x,y:x ~ y[assoced_equiv_rel]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num thy 1 Sections StandardLIB Doc