WhoCites Definitions mb collection Sections GenAutomata Doc

Who Cites col le?
col_leDef c1 c2 == x:T. x c1 x c2
Thm* T:Type, c1,c2:Collection(T). c1 c2 Prop
col_member Def x c == c(x)
Thm* T:Type, x:T, c:Collection(T). x c Prop

Syntax:c1 c2 has structure: col_le(T; c1; c2)

About:
applyuniversememberpropimpliesall!abstraction

WhoCites Definitions mb collection Sections GenAutomata Doc