M1,M2:MsgA, k:Knd. M1 
M2 
(M2.da(k) r M1.da(k))eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top)| Theorem | Name |
| M1,M2:MsgA, k:Knd. M1 M2 (M2.da(k) r M1.da(k)) | [ma-da-sub] |
| cites the following: | |
| eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top) | [subtype-fpf-cap-top] |