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]

Try larger context: GenAutomata