M1,M2:MsgA. M1 || M2 
M2 
M1 
M2B:(A
Type), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g g f g| Rank | Theorem | Name |
| 6 | M1,M2:MsgA. M1 || M2 M2 M1 M2 | [ma-sub-join-right] |
| cites the following: | ||
| 5 | B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g g f g | [fpf-sub-join-right] |