x
c.P(x)) == x:T. x c 
P(x)T:Type, c:Collection(T), P:(T
Prop). (xc.P(x)) Prop c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites col all? | |
| col_all | Def (xc.P(x)) == x:T. x c P(x) |
| Thm* T:Type, c:Collection(T), P:(TProp). (xc.P(x)) Prop | |
| col_member | Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | (xc.P(x)) | has structure: | col_all(T; c; x.P(x)) |
About:
 |  |  |  |  |  |  |  |