Nuprl - Definition Cascade for ReflectsProp

	Who Cites ReflectsProp?

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`

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

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

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

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

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

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

rev_implies	`Def P Q == Q P`

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

reps	`Def x = y == x t & x = y t`

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

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

About: