a,b:VCs. (a +* b) 
VCs a 
x bT:Type, a,b:Collection(T). (a + b) Collection(T) c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites vcs add? | |
| vcs_add | Def a +* b == a + b |
| Thm* a,b:VCs. (a +* b) VCs | |
| 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: | vcs_add(a; b) |
About:
 |  |  |  |  |  |  |