Some definitions of interest.
exists_unique	Def  !x:A. P(x) == x:A. x is the x:A. P(x)
	Thm*  A:Type, P:(AProp). (!x:A. P(x))  Prop
int_upper	Def  {i...} == {j:| ij }
	Thm*  n:. {n...}  Type
is_the	Def  x is the u:A. P(u) == P(x) & (u:A. P(u)  u = x)
	Thm*  A:Type, P:(AProp), x:A. (x is the x:A. P(x))  Prop
prime_factorization_of	Def  f is a factorization of k Def  == (x:Prime. k<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))
	Thm*  f:(Prime), k:. f is a factorization of k  Prop
prime_nats	Def  Prime == {x:| prime(x) }
nat	Def   == {i:| 0i }
	Thm*    Type

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