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

At: non nil is member 1

1. T: Type
2. eq: {T}
3. eq TT
4. x:T. eq(x,x)
5. x,y:T. eq(x,y) eq(y,x)
6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7. L: T List
8. L nil

x:T. x(eq) L

By: ListInd 7

Generated subgoals:

1 nil nil T List (x:T. x(eq) nil)
28. u: T
9. v: T List
10. v nil (x:T. x(eq) v)
u.v nil (x:T. x(eq) (u.v))

About:
listconsnilboolassertapplyfunctionuniversememberimpliesallexists

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