At: sigma decls mng value2 1 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
value(a)
rho(x)
By: Subst ((rho(x)) ~ [[x]] rho) 0
Generated subgoals:1 | (rho(x)) ~ [[x]] rho |
2 | value(a) [[x]] rho |
About: