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

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

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

By: Reduce 0 THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 5. InjCase(g(x,y) ; true; false)
x = y

2 5. x = y
InjCase(g(x,y) ; true; false)

About:

1	5. `InjCase(g(x,y) ; true; false)` `x = y`
2	5. `x = y` `InjCase(g(x,y) ; true; false)`