PrintForm Definitions mb collection Sections GenAutomata Doc

At: col equal inversion

T:Type, c1,c2:Collection(T). c1 = c2 c2 = c1
By:
Unfold `col_equal` 0
THEN
BackThruSomeHyp
Generated subgoals:

None

About:
universeimpliesall

PrintForm Definitions mb collection Sections GenAutomata Doc