(3steps) PrintForm Definitions mb collection Sections GenAutomata Doc

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

x c1
By: RevHypSubst -3 -1
Generated subgoals:

None

About:
universeequal

(3steps) PrintForm Definitions mb collection Sections GenAutomata Doc