Nuprl - Some Definitions

	Who Cites col?

col	`Def Collection(T) == TProp`

	`Thm* T:Type{i'}. col{i:l}(T) Type{i'}`

col_equal	`Def c1 = c2 == x:T. x c1 x c2`

	`Thm* T:Type, c1,c2:Collection(T). c1 = c2 Prop`

col_le	`Def c1 c2 == x:T. x c1 x c2`

	`Thm* T:Type, c1,c2:Collection(T). c1 c2 Prop`

col_member	`Def x c == c(x)`

	`Thm* T:Type, x:T, c:Collection(T). x c 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: