Some definitions of interest.
biject	Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)
	Thm* A,B:Type, f:(AB). Bij(A; B; f)  Prop
double_sum	Def sum(f(x;y) | x < n; y < m) == sum(sum(f(x;y) | y < m) | x < n)
	Thm* n,m:, f:(nm). sum(f(x,y) | x < n; y < m)
int_seg	Def {i..j} == {k:| i  k < j }
	Thm* m,n:. {m..n}  Type
nat	Def  == {i:| 0i }
	Thm*   Type
sum	Def sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x))
	Thm* n:, f:(n). sum(f(x) | x < n)

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