Who Cites col?
col	Def Collection(T) == TProp
	Thm* T:Type{i'}. col{i:l}(T) Type{i'}
col_filter	Def < x c | P(x) > (x) == x c & P(x)
	Thm* T:Type, c:Collection(T), Q:(TProp). < i c | Q(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: