Nuprl - Some Definitions

	Some definitions of interest.

f	`Def f(t) == SUBX(q(t); SUBX(X; Q(X)))`

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

repst	`Def x reps y == x reps y Term`

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

About: