(2steps) PrintForm Definitions Lemmas mb collection Sections GenAutomata Doc

At: col le reflexive

T:Type, c1:Collection(T). c1 c1
By:
Auto
THEN
BackThru Thm* c1,c2:Collection(T). c1 = c2 c1 c2
Generated subgoal:

11. T: Type
2. c1: Collection(T)
c1 = c1

About:
universeall

(2steps) PrintForm Definitions Lemmas mb collection Sections GenAutomata Doc