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

At: non nil is member 1 1 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. (nil = nil T List)False

x:T. x(eq) nil
By: Assert (nil = nil)
Generated subgoal:

19. nil = nil T List
x:T. x(eq) nil

About:
listnilboolassertapplyfunctionuniverseequal
memberimpliesfalseallexists

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