2. ds2: Collection(dec())
3. x: Label
4. y: Label
5. rho: Decl
6. v: [[d]] rho for d
{d:dec()| d ds1 }(x)7.
d:dec(). d ds2 
d.lbl = y mk_dec(x, d.typ) ds1
v [[d]] rho for d {d:dec()| d ds2 }(y) ds1,ds2:Collection(dec()), x,y:Label, rho:Decl, v:[[ds1]] rho(x).
(d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1) v [[ds2]] rho(y)| 1 | 1. ds1: Collection(dec()) 2. ds2: Collection(dec()) 3. x: Label 4. y: Label 5. rho: Decl 6. v: [[d]] rho for d {d:dec()| d ds1 }(x)7. d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1 v [[d]] rho for d {d:dec()| d ds2 }(y) |
About:
 |  |  |  |  |  |