Nuprl - Pf not equivalence implies not discrete eq 1 1

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

At: not equivalence implies not discrete eq 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. x: T
9. y: T
10. eq(x,y)
11. x,y:T. f(x,y) eq(x,y)

f(x,y)

By: DiscreteEq 7 THEN Analyze 0

Generated subgoal:

1 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

About:

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