Nuprl - Some Definitions

	Who Cites discrete equality?

discrete_equality	`Def {T=} == {eq:(TT)\| x,y:T. (eq(x,y)) x = y }`

	`Thm* T:Type. {T=} Type`

equivalence	`Def {T} == {f:(TT)\| (x:T. (f(x,x))) & (x,y:T. (f(x,y)) (f(y,x))) & (x,y,z:T. (f(x,y)) (f(y,z)) (f(x,z))) }`

	`Thm* T:Type{i}. {T} Type{i'}`

subtype	`Def S T == x:S. x T`

assert	`Def b == if b True else False fi`

	`Thm* b:. b Prop`

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

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

rev_implies	`Def P Q == Q P`

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

About: