At: decls mng member 1 1 1 1 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. d: dec()
8. d ds2
9. d.lbl =
x
d ds1
By:
EqLblFwd
THEN
BackThruSomeHyp
Generated subgoals:None
About:
