L:MsgA List. (A,B
L.A ||+ B) 
(M:MsgA. (BL.B ||+ M) 
(L) ||+ M)L:MsgA List. (A,BL.A ||+ B) (M:MsgA. (BL.M ||+ B) M ||+ (L))A,B:MsgA. A ||+ B B ||+ A| Rank | Theorem | Name |
| 10 | L:MsgA List. (A,BL.A ||+ B) (M:MsgA. (BL.B ||+ M) (L) ||+ M) | [ma-join-list-compat2] |
| cites the following: | ||
| 9 | L:MsgA List. (A,BL.A ||+ B) (M:MsgA. (BL.M ||+ B) M ||+ (L)) | [ma-join-list-compat] |
| 7 | A,B:MsgA. A ||+ B B ||+ A | [ma-compat-symmetry] |