Some definitions of interest.
fpf	Def a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
	Thm* A:Type, B:(AType). a:A fp-> B(a)  Type
fpf-empty	Def  == <nil,x.>
l_member	Def (x  l) == i:. i<||l|| & x = l[i]  T
	Thm* T:Type, x:T, l:T List. (x  l)  Prop

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