Nuprl - Pf sigma_decls_mng

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d2 d1 u ([[d2]] rho)

By: Unfold `sigma` 0 THEN Unfolds [`decl_type`;`subtype`] 0 THEN Reduce 0 THEN Try (Fold `decl` 0)

Generated subgoal:

1 1. d1: Collection(dec())
2. d2: Collection(dec())
3. rho: Decl
4. u: l:Labeldecl_type([[d1]] rho;l)
5. d2 d1
6. l: Label
7. x: [[d1]] rho(l)
x [[d2]] rho(l)

About:

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc