Some definitions of interest.
deq	Def EqDecider(T) == eq:TTx,y:T. x = y  (eq(x,y))
	Thm* T:Type. EqDecider(T)  Type
fpf-compatible	Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)
fpf-single	Def x : v == <[x],x.v>

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