Nuprl - Pf decls_mng

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

1. ds: Collection(dec())
2. rho: Decl
3. x: Label
4. y: [[d]] rho for d {d:dec()| d ds }(x)
5. a: SimpleType
6. mk_dec(x, a) ds

y [[a]] rho

By: AllHyps (i.(Unfold `dall` i) THEN (Reduce i) THEN (IsectHD mk_dec(x, a) i))

Generated subgoals:

1 4. y: d:{d:dec()| d ds }. [[d]] rho(x)
5. a: SimpleType
6. mk_dec(x, a) ds
mk_dec(x, a) = mk_dec(x, a) {d:dec()| d ds }

2 4. y: d:{d:dec()| d ds }. [[d]] rho(x)
5. a: SimpleType
6. mk_dec(x, a) ds
7. y [[mk_dec(x, a)]] rho(x)
y [[a]] rho

About:

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

1	4. `y:` `d:{d:dec()\| d ds }. [[d]] rho(x)` 5. `a:` `SimpleType` 6. `mk_dec(x, a) ds` `mk_dec(x, a) = mk_dec(x, a) {d:dec()\| d ds }`
2	4. `y:` `d:{d:dec()\| d ds }. [[d]] rho(x)` 5. `a:` `SimpleType` 6. `mk_dec(x, a) ds` 7. `y [[mk_dec(x, a)]] rho(x)` `y [[a]] rho`