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

At: is member non nil 1 1 1 1
1. T: Type
2. eq: {T=}
3. eq TT
4. x,y:T. eq(x,y) x = y
5. u: T
6. L: T List
7. u(eq) L
8. M: T List
9. N: T List

L = (nil @ (u.N)) (v:T, M:T List. L = v.M)
By:
Reduce 0
THEN
Analyze 0
Generated subgoal:

110. L = u.N
v:T, M:T List. L = v.M

About:
listconsnilboolassertapplyfunctionuniverse
equalmemberimpliesallexists

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