Some definitions of interest.
ma-empty	Def  == mk-ma(; ; ; ; ; ; ; )
fpf-empty	Def  == <nil,x.>
ma-sub	Def M1  M2 Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2)) Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2))) Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))) Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))) Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))
fpf-sub	Def f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)
msga	Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop
	Thm* MsgA  Type{i'}
top	Def Top == Void given Void
	Thm* Top  Type

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