Nuprl - Pf member dec lookup

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds

By: Unfold `dec_lookup` 0 THEN RW ColMemberC 0 THEN ExRepD

Generated subgoals:

1 1. ds: Collection(dec())
2. x: Label
3. T: SimpleType
4. d: dec()
5. d ds
6. d.lbl = x
7. T = d.typ
mk_dec(x, T) ds

2 1. ds: Collection(dec())
2. x: Label
3. T: SimpleType
4. mk_dec(x, T) ds
d:dec(). d ds & d.lbl = x & T = d.typ

About:

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

1	1. `ds:` `Collection(dec())` 2. `x:` `Label` 3. `T:` `SimpleType` 4. `d:` `dec()` 5. `d ds` 6. `d.lbl = x` 7. `T = d.typ` `mk_dec(x, T) ds`
2	1. `ds:` `Collection(dec())` 2. `x:` `Label` 3. `T:` `SimpleType` 4. `mk_dec(x, T) ds` `d:dec(). d ds & d.lbl = x & T = d.typ`