M1,M2,M3:MsgA. M1 
M2 
M2 M3 M1 M3Thm*
Thm* (
B:(A
Type), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'),
Thm* (
f,g:a:A fp-> B(a). (a:A. B(a) r C(a)) f g f g)| Rank | Theorem | Name |
| 7 | M1,M2,M3:MsgA. M1 M2 M2 M3 M1 M3 | [ma-sub_transitivity] |
| cites the following: | ||
| 6 | Thm*
Thm* ( B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'),
Thm* ( f,g:a:A fp-> B(a). (a:A. B(a) r C(a)) f g f g) | [fpf-sub_functionality] |