Who Cites col equal? | |
col_equal | Def c1 = c2 == x:T. x c1 x c2 |
Thm* T:Type, c1,c2:Collection(T). c1 = c2 Prop | |
col_member | Def x c == c(x) |
Thm* T:Type, x:T, c:Collection(T). x c Prop | |
iff | Def P Q == (P Q) & (P Q) |
Thm* A,B:Prop. (A B) Prop | |
rev_implies | Def P Q == Q P |
Thm* A,B:Prop. (A B) Prop |
Syntax: | c1 = c2 | has structure: | col_equal(T; c1; c2) |
About: