mb
collection
Sections
GenAutomata
Doc
Theorem
Name
Thm*
c1:Collection(T). c1
c1
[col_le_reflexive]
cites
Thm*
c1,c2:Collection(T). c1 = c2
c1
c2
[col_le_weakening]
mb
collection
Sections
GenAutomata
Doc
c1:Collection(T). c1 
c1c1,c2:Collection(T). c1 = c2 
c1 c2c1:Collection(T). c1 c1c1,c2:Collection(T). c1 = c2 c1 c2