(5steps) PrintForm Definitions Lemmas core 3 jlc Sections Support(jlc) Doc

At: not equivalence implies not discrete eq 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. f: {T=}
8. f TT
9. x,y:T. f(x,y) x = y
10. x: T
11. y: T
12. eq(x,y)
13. x,y:T. f(x,y) eq(x,y)
14. f(x,y)

False

By: FwdThru 13 [14]

Generated subgoal:

115. eq(x,y)
False

About:
boolassertapplyfunctionuniverseequalmemberimpliesfalseall

(5steps) PrintForm Definitions Lemmas core 3 jlc Sections Support(jlc) Doc