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

1. T: Type
2. g: x,y:T. (x = y)+(x = y)
3. x: T
4. y: T

InjCase(g(x,y) ; true; false) x = y

By: Witness2 x THEN RevHypSubst -1 0

Generated subgoal:

1 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)
InjCase(y1(y) ; true; false) x = y

About: