Nuprl - Some Definitions

	Some definitions of interest.

ReflectsProp	`Def ReflectsProp(P; qP; Tr) == t,qt:Term. qt reps t {Tr(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 reps y == x reps y Term`

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

s	`Def s(t) == f(t)/q(f(t))`

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

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

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

About: