a 
x b
T:Type, a,b:Collection(T). (a + b) Collection(T) c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites col add? | |
| col_add | Def (a + b)(x) == x a x b |
| Thm* T:Type, a,b:Collection(T). (a + b) Collection(T) | |
| col_member | Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | a + b | has structure: | col_add(a; b) |
About:
 |  |  |  |  |  |  |