Nuprl - Pf discrete implies discrete equality 1 1 1 1 2 1 1 1 1

(13steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete implies discrete equality 1 1 1 1 2 1 1 1 1

1. T: Type
2. g: x:Ty:T. (x = y)+(x = y)
3. x: T
4. y: T
5. y1: y:T(x = y)+(x = y)
6. y1 = g(x) (y:T. (x = y)+(x = y))
7. y2: (x = y)+(x = y)
8. y2 = y1(y)

InjCase(y2 ; true; false) x = y

By: Analyze 7 THEN Reduce 0

Generated subgoal:

1 7. y3: x = y
8. inr(y3) = y1(y)
9. x = y
False

About:

(13steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc