Nuprl - Some Definitions

	Some definitions of interest.

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

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

subx	`Def SUBX(t; e) == t[e/X]`

	`Thm* t,r:Term. SUBX(t; r) Term`

About: