Nuprl - Some Definitions

	Some definitions of interest.

f	`Def f(t) == SUBX(t; SUBX(X; UP(X)))`

	`Thm* t:Term. f(t) Term`

repst	`Def x = y == x = y`

	`Thm* t,x:Term. (t = x) Prop`

About: