(3steps) PrintForm Definitions mb collection Sections GenAutomata Doc

At: col equal weakening

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

11. T: Type
2. c1: Collection(T)
3. c2: Collection(T)
4. c1 = c2
5. x: T
6. x c1
x c2
21. T: Type
2. c1: Collection(T)
3. c2: Collection(T)
4. c1 = c2
5. x: T
6. x c2
x c1

About:
universeequalimpliesall

(3steps) PrintForm Definitions mb collection Sections GenAutomata Doc