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

At: sublist reflexive 1 2
1. T: Type
2. eq: {T=}
3. L: T List
4. u: T
5. v: T List
6. v(eq)v

v(eq)(u.v)
By: BackThru Thm* eq:{T=}, u:T, v:T List. v(eq)(u.v)
Generated subgoals:

None

About:
listconsuniverse

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