M1,M2:MsgA. M1 
M1 
M2B1,B2:(A
Type), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
Thm* f
f g| Rank | Theorem | Name |
| 6 | M1,M2:MsgA. M1 M1 M2 | [ma-sub-join-left] |
| cites the following: | ||
| 5 | B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
Thm* f f g | [fpf-sub-join-left] |