M1,M2:MsgA.
Thm* M1
M2
Thm*
Thm* (
k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x).
Thm* (M2.ef(k,x,s,v,w)
M1.ef(k,x,s,v,w))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.
Thm* M1 M2
Thm*
Thm* ( k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x).
Thm* (M2.ef(k,x,s,v,w) M1.ef(k,x,s,v,w)) | [ma-ef-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] |