is mentioned by

Thm* 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)

[decls_mng_rename_member]

In prior sections: mb automata 2

Try larger context: GenAutomata