is mentioned by

Thm* P:(TProp), c1,c2:Collection(T). c1 = c2 ((xc1.P(x)) (xc2.P(x)))	[col_all_functionality]
Thm* c:Collection(T), P:(TProp). (xc.P(x)) (x:T. x c P(x))	[col_all_iff]
Thm* f:(TProp), c:Collection(T), x:T. x < i c | f(i) > x c & f(x)	[member_col_filter]
Def Collection(T) == TProp	[col]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1

Try larger context: GenAutomata