At: decls mng member 1 1 1 2 1 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. x: Label
4. rho: Decl
5. v: 
d:{d:dec()| d 
ds1 }. [[d]] rho(x)
6. 
d:dec(). d ds2 
d.lbl = x d ds1
7. lbl: Label
8. d1: SimpleType
9. < lbl,d1 > ds2
10. 
lbl =
x
11. x = lbl
v [[d1]] rho
By:
Analyze -2
THEN
EqLblFwd
THEN
HypSubst -1 0
THEN
EqLblReflexive 0
Generated subgoals:None
About:
