Nuprl - Pf discrete equality inc equivalence 1

(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

1. T: Type
2. x: {T=}

x {T}

By: DiscreteEq 2 THEN Analyze

Generated subgoals:

1 3. x TT
4. x@0,y:T. x(x@0,y) x@0 = y
x TT

2 3. x TT
4. x@0,y:T. x(x@0,y) x@0 = y
5. x@0: T
x(x@0,x@0)

3 3. x TT
4. x@0,y:T. x(x@0,y) x@0 = y
5. x@0: T
6. y: T
7. x(x@0,y)
x(y,x@0)

4 3. x TT
4. x@0,y:T. x(x@0,y) x@0 = y
5. x@0: T
6. y: T
7. x(y,x@0)
x(x@0,y)

5 3. x TT
4. x@0,y:T. x(x@0,y) x@0 = y
5. x@0: T
6. y: T
7. z: T
8. x(x@0,y)
9. x(y,z)
x(x@0,z)

About:

(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

1	3. `x TT` 4. `x@0,y:T. x(x@0,y) x@0 = y` `x TT`
2	3. `x TT` 4. `x@0,y:T. x(x@0,y) x@0 = y` 5. `x@0:` `T` `x(x@0,x@0)`
3	3. `x TT` 4. `x@0,y:T. x(x@0,y) x@0 = y` 5. `x@0:` `T` 6. `y:` `T` 7. `x(x@0,y)` `x(y,x@0)`
4	3. `x TT` 4. `x@0,y:T. x(x@0,y) x@0 = y` 5. `x@0:` `T` 6. `y:` `T` 7. `x(y,x@0)` `x(x@0,y)`
5	3. `x TT` 4. `x@0,y:T. x(x@0,y) x@0 = y` 5. `x@0:` `T` 6. `y:` `T` 7. `z:` `T` 8. `x(x@0,y)` 9. `x(y,z)` `x(x@0,z)`