Some definitions of interest.
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
da-outlinks	Def da-outlinks(da;i) Def == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
fpf-single	Def x : v == <[x],x.v>
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
l_member	Def (x  l) == i:. i<||l|| & x = l[i]  T
	Thm* T:Type, x:T, l:T List. (x  l)  Prop
lnk	Def lnk(k) == 1of(outl(k))
	Thm* k:Knd. isrcv(k)  lnk(k)  IdLnk
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
mapfilter	Def mapfilter(f;P;L) == map(f;filter(P;L))
	Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List. Thm* mapfilter(f;P;L)  T' List
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
tagof	Def tag(k) == 2of(outl(k))
	Thm* k:Knd. isrcv(k)  tag(k)  Id
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))

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