Some definitions of interest.
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
nat	Def  == {i:| 0i }
	Thm*   Type
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
mu	Def mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi  (recursive)
	Thm* f:(). (n:. f(n))  mu(f)

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