Thms Turing Sections NuprlLIB Doc

tm_q Def (p) == 1of(p)

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

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

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