WhoCites Definitions mb automata 4 Sections GenAutomata Doc

Who Cites col equal?
col_equalDef 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:
applyuniversememberpropimpliesandall!abstraction

WhoCites Definitions mb automata 4 Sections GenAutomata Doc