(3steps) PrintForm Definitions mb collection Sections GenAutomata Doc

At: col equal weakening 1
1. T: Type
2. c1: Collection(T)
3. c2: Collection(T)
4. c1 = c2
5. x: T
6. x c1

x c2
By: HypSubst -3 -1
Generated subgoals:

None

About:
universeequal

(3steps) PrintForm Definitions mb collection Sections GenAutomata Doc