Nuprl - Pf discrete implies bool equality 1 1 1

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

At: discrete implies bool equality 1 1 1

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

f:(TT). x,y:T. f(x,y) x = y

By: With (x,y. InjCase(g(x,y) ; true; false)) (Analyze 0)

Generated subgoals:

1 3. x: T
4. y: T
InjCase(g(x,y) ; true; false)

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

3 3. f: TT
4. x: T
5. y: T
f(x,y)

About:

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