Some definitions of interest.
hcurry	Def curry == f:'a'b'c. x:'a. y:'b. f(<x,y>)
	Thm* 'a,'b,'c:S. curry  ((hprod('a; 'b)  'c)  'a  'b  'c)
hfun	Def 'a  'b == 'a'b
	Thm* 'a,'b:S. ('a  'b)  S
hprod	Def hprod('a; 'b) == 'a'b
	Thm* 'a,'b:S. hprod('a; 'b)  S
label	Def t  ...$L == t
stype	Def S == {T:Type| x:T. True }
	Thm* S  Type{2}

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