Thms Turing Sections NuprlLIB Doc

tm_proto_sigma Def P(p) == 1of(2of(p))

Thm* p:PM{i}. P(p) Type

pi2 Def 2of(t) == t.2

Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))

pi1 Def 1of(t) == t.1

Thm* B:(AType), p:a:AB(a). 1of(p) A