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

At: sublist weakening wrt identity 1
1. T: Type
2. Discrete{T}
3. eq: {T}
4. L: T List
5. M: T List
6. L = M

L(eq)M
By: RevHypSubst 6 0 THENA Equivalence 3
Generated subgoal:

1 L(eq)L

About:
listuniverseequal

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