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