Nuprl - Pf sigma_decls_mng

1. ds: Collection(dec())
2. rho: Decl
3. a: ([[ds]] rho)
4. x: Label
5. mk_dec(kind(a), x) ds

value(a) rho(x)

By: Inst Thm* ds:Collection(dec()), rho:Decl, a:([[ds]] rho). value(a) [[dec_lookup(ds;kind(a))]] rho [ds;rho;a]

Generated subgoal:

1 6. value(a) [[dec_lookup(ds;kind(a))]] rho
value(a) rho(x)

About: