PrintForm
Definitions
mb
collection
Sections
GenAutomata
Doc
At:
col
all
functionality
T:Type, P:(T
Prop), c1,c2:Collection(T). c1 = c2
((
x
c1.P(x))
(
x
c2.P(x)))
By:
Unfold `col_all` 0
THEN
UnivCD
THEN
RW (SweepDnC (HypC -1)) 0
THEN
BackThruSomeHyp
Generated subgoals:
None
About:
PrintForm
Definitions
mb
collection
Sections
GenAutomata
Doc
T:Type, P:(T
Prop), c1,c2:Collection(T). c1 = c2 
((x
c1.P(x)) 
(xc2.P(x)))
