Def MsgAForm
Def == x:Id fp-> Topx:Knd fp-> Typex:Id fp-> Topx:Id fp-> Top
Def == x:KndId fp-> Topx:KndIdLnk fp-> Topx:Id fp-> Topx:IdLnkId fp-> Top
Def == Top

is mentioned by

Thm* A,B:MsgAForm, ltg:(IdLnkIdType), i:Id. Thm* (ltg  ma-outlinks(A  B;i)) Thm*  Thm* (ltg  ma-outlinks(A;i))  (ltg  ma-outlinks(B;i))	[ma-outlinks-join]
Thm* L:MsgA List. (L)  MsgAForm	[msg-form-join-list]
Thm* A,B:MsgAForm. A  B  MsgAForm	[msg-form-join]
Thm* M:MsgAForm, i:Id. ma-outlinks(M;i)  (IdLnkIdType) List	[ma-outlinks-wf2]
Thm* MsgA r MsgAForm	[msga-sub-msg-form]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html