(9steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: sublist weakening wrt identity

T:Type. Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M)
By: UnivCD
Generated subgoal:

11. T: Type
2. Discrete{T}
3. eq: {T}
4. L: T List
5. M: T List
6. L = M
L(eq)M

About:
listuniverseequalimpliesall

(9steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc