At: decls mng functionality sigma 1 1 1 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. l: Label
5. r1: [[ds1]] rho(l)
6. ds1 = ds2
7. d: dec()
8. d 
ds2
9. d.lbl = l
d ds1
By:
AllHyps (Unfold `col_equal`)
THEN
BackThruSomeHyp
Generated subgoals:None
About:
