Some definitions of interest.
bi-graph	Def bi-graph(G;to;from) Def == i:|G|.  Def == (lto(i).destination(l) = i Def == & (G(source(l))) Def == & (l  from(source(l))) Def == & (lnk-inv(l)  from(i))) Def == & (lfrom(i).source(l) = i Def == & & (G(destination(l))) Def == & & (l  to(destination(l))) Def == & & (lnk-inv(l)  to(i)))
bi-graph-edge	Def Edge(G) == {l:IdLnk| i:|G|. (l  from(i)) }
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
rset	Def |R| == {i:Id| (R(i)) }
	Thm* R:(Id). |R|  Type
Id	Def Id == Atom
	Thm* Id  Type
bi-graph-inv	Def inverse(l) == lnk-inv(l)
lnk-inv	Def lnk-inv(l) == <1of(2of(l)),1of(l),2of(2of(l))>

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