Nuprl - Some Definitions

tm_config	`Def Config(M) == (M)(G(M))` `Thm* M:PM{i}. Config(M) Type`
tm_gamma	`Def G(p) == P(p)+P(p)` `Thm* M:PM{i}. G(M) Type`
tm_q	`Def (p) == 1of(p)` `Thm* p:PM{i}. (p) Type`
tm_proto_pi	`Def P(p) == 1of(2of(2of(p)))` `Thm* p:PM{i}. P(p) Type`
tm_proto_sigma	`Def P(p) == 1of(2of(p))` `Thm* p:PM{i}. P(p) Type`
pi1	`Def 1of(t) == t.1` `Thm* B:(AType), p:a:AB(a). 1of(p) A`
pi2	`Def 2of(t) == t.2` `Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))`