At: sigma decls mng value2 1 1 2 1
1. ds: Collection(dec())
2. rho: Decl
3. a: ([[ds]] rho)
4. x: Label
5. mk_dec(kind(a), x) ds
6. value(a) [[dec_lookup(ds;kind(a))]] rho
x dec_lookup(ds;kind(a))
By: RWO "member_dec_lookup" 0
Generated subgoals:None
About: