is mentioned by

Thm* c:Collection(T), f:(TCollection(T')), y:T'. y (xc.f(x)) (x:T. x c & y f(x))	[member_col_accum]
Thm* c:Collection(T), f:(TT'), x:T'. x < f(y) | y c > (y:T. y c & x = f(y))	[member_col_map]
Thm* f:(TProp), c:Collection(T), x:T. x < i c | f(i) > x c & f(x)	[member_col_filter]
Def (xc.f(x))(y) == x:T. x c & y f(x)	[col_accum]
Def < f(x) | x c > (y) == x:T. x c & y = f(x) T'	[col_map]
Def < x c | P(x) > (x) == x c & P(x)	[col_filter]

In prior sections: core int 1 bool 1 int 2 fun 1

Try larger context: GenAutomata