Some definitions of interest.
Id	Def Id == Atom
	Thm* Id  Type
decidable	Def Dec(P) == P  P
	Thm* A:Prop. Dec(A)  Prop
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-all	Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))
fpf-single	Def x : v == <[x],x.v>
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)

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