x
c.f(x))(y) == 
x:T. x c & y f(x)
T,T':Type, f:(T
Collection(T')), c:Collection(T). (xc.f(x)) Collection(T') c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites col accum? | |
| col_accum | Def (xc.f(x))(y) == x:T. x c & y f(x) |
| Thm* T,T':Type, f:(TCollection(T')), c:Collection(T). (xc.f(x)) Collection(T') | |
| col_member | Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | (xc.f(x)) | has structure: | col_accum(T; c; x.f(x)) |
About:
 |  |  |  |  |  |  |  |  |