Nuprl - Some Definitions

	Some definitions of interest.

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

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

subx	`Def t/e == t[e/X]`

	`Thm* t,r:Term. t/r Term`

About: