Nuprl - Pf sigma_decls_mng

1. d1: Collection(dec())
2. d2: Collection(dec())
3. rho: Decl
4. l: Label
5. u1: decl_type([[d1]] rho;l)
6. d1 = d2

u1 [[dec_lookup(d2;l)]] rho

By: Unfold `sts_mng` 0 THEN Analyze THEN Analyze -1 THEN Unfolds [`decl_type`] -4 THEN Reduce -4

Generated subgoal:

1 5. u1: [[d1]] rho(l)
6. d1 = d2
7. x: SimpleType
8. x dec_lookup(d2;l)
u1 [[x]] rho

About: