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

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

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

1. T: Type
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)
8. y2: (y = y)+(y = y)
9. y2 = y1(y)

InjCase(y2 ; true; false)

By: Analyze 8 THEN Reduce 0

Generated subgoals:

1 8. x1: y = y
9. inl(x1) = y1(y)
True

2 8. y3: y = y
9. inr(y3) = y1(y)
False

About:

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

1	8. `x1:` `y = y` 9. `inl(x1) = y1(y)` `True`
2	8. `y3:` `y = y` 9. `inr(y3) = y1(y)` `False`