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

At: is member cons 1 2 1

1. T: Type
2. eq: {T}
3. t: T
4. L: T List
5. eq(t,t) = false

eq(t,t)

By: Equivalence 2

Generated subgoal:

13. 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. t: T
8. L: T List
9. eq(t,t) = false
eq(t,t)

About:
listboolbfalseassertapplyuniverseequal

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