is mentioned by

Thm* L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.B ||+ M)  (L) ||+ M)	[ma-join-list-compat2]
Thm* L:MsgA List. (A,BL.A ||+ B)  (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-compat]
Thm* L:MsgA List. (A,BL.A ||+ B)  (AL.Feasible(A))  Feasible((L))	[ma-join-list-feasible]
Thm* L:MsgA List, M:MsgA. (A,BL.A ||+ B)  (M  L)  M  (L)	[ma-sub-join-list]
Thm* L:MsgA List. (A,BL.A ||+ B)  (L)  MsgA	[ma-join-list_wf]
Thm* L:MsgA List.  Thm* (A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL.M ||+ B)  M ||+ (L))	[ma-join-list-property]
Thm* A,B,C:MsgA. A ||+ B  C ||+ A  C ||+ B  C ||+ A  B	[ma-compat-join]
Thm* A:MsgA. A ||+	[ma-empty-compat-right]
Thm* A:MsgA.  ||+ A	[ma-empty-compat-left]
Thm* A,B:MsgA. A ||+ B  B ||+ A	[ma-compat-symmetry]

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