Nuprl - Some Definitions

	Some definitions of interest.

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

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

iff	`Def P Q == (P Q) & (P Q)`

	`Thm* A,B:Prop. (A B) Prop`

not	`Def A == A False`

	`Thm* A:Prop. (A) 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: