is mentioned by

Thm* c:Collection(T), P:(TProp). (xc.P(x)) (x:T. x c P(x))	[col_all_iff]
Thm* l:Collection(T) List, x:T List. x col_list_prod(l) ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])	[member_col_list_prod]
Thm* c:Collection(T), f:(TCollection(T')), y:T'. y (xc.f(x)) (x:T. x c & y f(x))	[member_col_accum]
Thm* a,b:Collection(T), x:T. x a + b x a x b	[member_col_add]
Thm* c:Collection(T), f:(TT'), x:T'. x < f(y) | y c > (y:T. y c & x = f(y))	[member_col_map]
Thm* C:(ICollection(T)), x:T. x i:I. C(i) (i:I. x C(i))	[member_col_union]
Thm* f:(TProp), c:Collection(T), x:T. x < i c | f(i) > x c & f(x)	[member_col_filter]
Thm* c1,c2:Collection(T), t1,t2:T. t1 = t2 c1 = c2 (t1 c1 t2 c2)	[col_member_functionality]
Thm* T:Type{i'}, x:T. x < > False	[member_col_none]
Def (xc.P(x)) == x:T. x c P(x)	[col_all]
Def col_list_prod(l)(x) == ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])	[col_list_prod]
Def (xc.f(x))(y) == x:T. x c & y f(x)	[col_accum]
Def (a + b)(x) == x a x b	[col_add]
Def < f(x) | x c > (y) == x:T. x c & y = f(x) T'	[col_map]
Def (i:I. C(i))(x) == i:I. x C(i)	[col_union]
Def < x c | P(x) > (x) == x c & P(x)	[col_filter]
Def c1 c2 == x:T. x c1 x c2	[col_le]
Def c1 = c2 == x:T. x c1 x c2	[col_equal]

Try larger context: GenAutomata