Nuprl - Pf sigma_decls_mng

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

By: Auto THEN Analyze 3 THEN All (Unfold `decl_type`) THEN All Reduce

Generated subgoal:

1 1. ds: Collection(dec())
2. rho: Decl
3. l: Label
4. a1: [[ds]] rho(l)
a1 [[dec_lookup(ds;l)]] rho

About: