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