At: decls mng rename member 1 1 1 1 2 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. x: Label
4. y: Label
5. rho: Decl
6. v: 
d:{d:dec()| d 
ds1 }. [[d]] rho(x)
7. 
d:dec(). d ds2 
d.lbl = y mk_dec(x, d.typ) ds1
8. d: {d:dec()| d ds2 }
9. d.lbl =
y
10. v [[d.typ]] rho
v [[d]] rho(y)
By:
Analyze -3
THEN
Analyze -4
THEN
Unfold `dec_mng` 0
THEN
Unfold `dbase` 0
THEN
All Reduce
THEN
SplitOnConclITE
Generated subgoals:None
About:
