Nuprl - Pf ioa all mng state 1 1 1

(9steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. I: Type
2. A: Iioa{i:l}()
3. rho: Decl
4. de: sig()
5. e: {[[de]] rho}
6. s: l:Labeldecl_type([[ioa_all(I; i.A(i)).ds]] rho;l)
7. i: I
8. x1: Label

decl_type([[ioa_all(I; i.A(i)).ds]] rho;x1) decl_type([[A(i).ds]] rho;x1)

By: Unfolds [`subtype`;`decl_type`] 0

Generated subgoals:

1 9. x: [[ioa_all(I; i.A(i)).ds]] rho(x1)
x [[A(i).ds]] rho(x1)

2 [[ioa_all(I; i.A(i)).ds]] rho LabelType

About:

(9steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1	9. `x:` `[[ioa_all(I; i.A(i)).ds]] rho(x1)` `x [[A(i).ds]] rho(x1)`
2	`[[ioa_all(I; i.A(i)).ds]] rho LabelType`