Nuprl - Some Definitions

	Some definitions of interest.

ReflectsProp	`Def ReflectsProp(P; qP; Tr) == t,qt:Term. qt = t {Tr(SUBX(qP; qt)) Tr(t)}`

	`Thm* P:(TermProp), qP:Term, L:(TermProp). ReflectsProp(P; qP; L) Prop`

RespectsNot	`Def RespectsNot(Tr; L) == t:Term. Tr(NOT(t)) L(t) & Tr(t)`

	`Thm* Tr,L:(TermProp). RespectsNot(Tr; L) Prop`

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

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

s	`Def s(t) == SUBX(f(t); f(t))`

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

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

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

About: