d1,d2:Collection(dec()), rho:Decl, u:(
[[d1]] rho).
d2 
d1 
u 
([[d2]] rho)ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x).
(d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x)| Theorem | Name |
|
Thm* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho).
d2 d1 u ([[d2]] rho) | [sigma_decls_mng_monotone] |
| cites | |
|
Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x).
(d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x) | [decls_mng_member] |