At: sigma decls mng2 1 1 1 1 1 1 1 1
1. da: Collection(dec())
2. rho: Decl
3. k: Label
4. w: [[dec_lookup(da;k)]] rho
5. lbl: Label
6. d1: SimpleType
7. < lbl,d1 > 
da
8. k =
lbl
9. k = lbl
d1 dec_lookup(da;k)
By:
RWW "member_dec_lookup" 0
THEN
HypSubstSq -1 0
THEN
Unfold `mk_dec` 0
Generated subgoals:None
About:
