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* 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* a1,b1,a2,b2:Collection(T). a1 = b1 a2 = b2 (a1 = a2 b1 = b2)	[col_equal_functionality]
Thm* a,b,c:Collection(T). a b b c a c	[col_le_transitivity]
Thm* c1,c2:Collection(T). c1 = c2 c1 c2	[col_le_weakening]
Thm* c1,c2:Collection(T), t1,t2:T. t1 = t2 c1 = c2 (t1 c1 t2 c2)	[col_member_functionality]
Thm* c1,c2,c3:Collection(T). c1 = c2 c2 = c3 c1 = c3	[col_equal_transitivity]
Thm* c1,c2:Collection(T). c1 = c2 c2 = c1	[col_equal_inversion]
Thm* c1,c2:Collection(T). c1 = c2 c1 = c2	[col_equal_weakening]
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 c1 c2 == x:T. x c1 x c2	[col_le]

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

Try larger context: GenAutomata