Nuprl - Pf decls_mng_record

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

ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}

By: Unfold `record` 0 THEN Unfolds [`subtype`;`decl_type`] 0

Generated subgoals:

1 1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Labeldecl_type([[ds1]] rho;l)
5. ds2 ds1
6. x1: Label
7. x: [[ds1]] rho(x1)
x [[ds2]] rho(x1)

2 1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Labeldecl_type([[ds1]] rho;l)
5. ds2 ds1
6. x1: Label
[[ds1]] rho LabelType

About:

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

1	1. `ds1:` `Collection(dec())` 2. `ds2:` `Collection(dec())` 3. `rho:` `Decl` 4. `r:` `l:Labeldecl_type([[ds1]] rho;l)` 5. `ds2 ds1` 6. `x1:` `Label` 7. `x:` `[[ds1]] rho(x1)` `x [[ds2]] rho(x1)`
2	1. `ds1:` `Collection(dec())` 2. `ds2:` `Collection(dec())` 3. `rho:` `Decl` 4. `r:` `l:Labeldecl_type([[ds1]] rho;l)` 5. `ds2 ds1` 6. `x1:` `Label` `[[ds1]] rho LabelType`