Nuprl - mb_automata_3 LEMMAs for sigma_decls_mng

Rank	Theorem	Name
2	Thm* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d1 = d2 u ([[d2]] rho)	[sigma_decls_mng_functionality]
cites
1	Thm* da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho. < k,w > ([[da]] rho)	[sigma_decls_mng2]
0	Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho	[decls_mng_subtype]