Turing Sections NuprlLIB Doc

conf_hd Def t.hd == 2of(2of(t))

Thm* M:PM{i}, t:Config(M). t.hd

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

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