Who Cites col?
col	Def Collection(T) == TProp
	Thm* T:Type{i'}. col{i:l}(T) Type{i'}
col_union	Def (i:I. C(i))(x) == i:I. x C(i)
	Thm* T,I:Type, C:(ICollection(T)). (i:I. C(i)) Collection(T)
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: