Nuprl - Pf discrete implies discrete equality 1 1 1 1

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

At: discrete implies discrete equality 1 1 1 1

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

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

By: Unfold `discrete_equality` 0 THEN AbSetMemEqTypeCD

Generated subgoals:

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

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

3 3. eq: TT
(x,y:T. eq(x,y) x = y) Type

About:

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