Some definitions of interest.
fpf-ap	Def f(x) == 2of(f)(x)
fpf-single	Def x : v == <[x],x.v>
top	Def Top == Void given Void
	Thm* Top  Type

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