Turing Sections NuprlLIB Doc

Def _(p) == 1of(2of(2of(2of(p))))

Thm* p:PM{i}. _(p) (p) blank_pi

Thm* p:PM{i}. _(p) Void+P(p) blank_proto_pi