At: sigma decls mng functionality 1 1
1. d1: Collection(dec())
2. d2: Collection(dec())
3. rho: Decl
4. l: Label
5. u1: [[d1]] rho(l)
6. d1 = d2
7. x: SimpleType
8. x 
dec_lookup(d2;l)
u1 [[x]] rho
By: Using [`ds',d1;`x',l]
(BackThru
Thm* 
ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds 
y [[a]] rho)
Generated subgoal:| 1 | mk_dec(l, x) d1 |
About:
