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

At: is member cons 1 1
1. T: Type
2. eq: {T}
3. t: T
4. L: T List
5. eq(t,t) = true

true
By: BackThru Thm* P:. P P = true
Generated subgoals:

None

About:
listboolbtrueassertapplyuniverseequal

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