Nuprl - rel_1 LEMMAs for trans_rel_func_wrt_sym

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
Thm* R:(TTProp). Thm* (Trans x,y:T. R(x,y)) Thm* Thm* (a,a',b,b':T. Thm* (Symmetrize(x,y.R(x,y);a;b) Thm* ( Thm* (Symmetrize(x,y.R(x,y);a';b') (R(a,a') R(b,b')))	[trans_rel_func_wrt_sym_self]
cites the following:
Thm* R:(TTProp). Thm* (Trans x,y:T. R(x,y)) Thm* Thm* (a,a',b,b':T. R(b,a) R(a',b') R(a,a') R(b,b'))	[trans_rel_self_functionality]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html