At: decls mng monotone 1 1 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Label
[[ds1]] rho(l)
5. ds2 
ds1
6. x1: Label
7. x: [[ds1]] rho(x1)
8. d: dec()
9. d 
ds2
10. d.lbl = x1
d ds1
By:
AllHyps (Unfold `col_le`)
THEN
BackThruSomeHyp
Generated subgoals:None
About:
