Some definitions of interest.
ma-join-list	Def (L) == reduce(A,B. A  B;;L)
ma-join	Def M1  M2 Def == mk-ma(1of(M1)  1of(M2); Def == mk-ma(1of(2of(M1))  1of(2of(M2)); Def == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2))); Def == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))); Def == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of( Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(M2)))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2))))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))
ma-outlinks	Def ma-outlinks(M;i) == da-outlinks(1of(2of(M));i)
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'}
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
l_all	Def (xL.P(x)) == x:T. (x  L)  P(x)
	Thm* T:Type, L:T List, P:(TProp). (xL.P(x))  Prop
ma-empty	Def  == mk-ma(; ; ; ; ; ; ; )

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html