L:MsgA List. (A,B
L.A ||+ B) 
(L) MsgAL:MsgA List.
Thm* (
A,BL.A ||+ B) (L) MsgA & (M:MsgA. (BL.M ||+ B) M ||+ (L))| Rank | Theorem | Name |
| 9 | L:MsgA List. (A,BL.A ||+ B) (L) MsgA | [ma-join-list_wf] |
| cites the following: | ||
| 8 | L:MsgA List.
Thm* ( A,BL.A ||+ B) (L) MsgA & (M:MsgA. (BL.M ||+ B) M ||+ (L)) | [ma-join-list-property] |