Q == P + Q
P,Q:Fmla. (P Q) 
Fmla 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 pred and? | |
| pred_and | Def P Q == P + Q |
| Thm* P,Q:Fmla. (P Q) Fmla | |
| 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: | P Q | has structure: | pred_and(P; Q) |
About:
 |  |  |  |  |  |  |