Turing Sections NuprlLIB Doc

tm_r Def p.r == 2of(2of(2of(2of(2of(2of(2of(p)))))))

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

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

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