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

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

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

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

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

By: Unfold `all` 2 THEN Witness2 y

Generated subgoal:

1 2. g: x,y:T(x = y)+(x = y)
3. x: T
4. y: T
5. x = y
6. y1: y@0:T(y = y@0)+(y = y@0)
7. y1 = g(y)
InjCase(g(y,y) ; true; false)

About:

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