Some definitions of interest.
Kind-deq	Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
Id	Def Id == Atom
	Thm* Id  Type
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>

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