da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho.
< k,w > 
(
[[da]] rho)sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType.
s sts 
v [[s]] rho| Theorem | Name |
|
Thm* da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho.
< k,w > ([[da]] rho) | [sigma_decls_mng2] |
| cites | |
|
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType.
s sts v [[s]] rho | [sts_mng_subtype] |