Nuprl - Pf sigma_decls_mng2 1 1 1 1 1 1

1. da: Collection(dec())
2. rho: Decl
3. k: Label
4. w: [[dec_lookup(da;k)]] rho
5. d: dec()
6. d da

w [[d]] rho(k)

By: Unfold `dec_mng` 0 THEN Analyze -2 THEN Reduce 0 THEN Fold `decl_type` 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoal:

1 5. lbl: Label
6. d1: SimpleType
7. < lbl,d1 > da
8. k = lbl
w [[d1]] rho

About: