PrintForm Definitions mb collection Sections GenAutomata Doc

At: col equal transitivity

T:Type, c1,c2,c3:Collection(T). c1 = c2 c2 = c3 c1 = c3
By:
Unfold `col_equal` 0
THEN
BackThruSomeHyp
THEN
AllHyps (i.(BackThru i) THEN (Complete Auto))
Generated subgoals:

None

About:
universeimpliesall

PrintForm Definitions mb collection Sections GenAutomata Doc