Nuprl - Pf discrete equality is equivalence 1

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

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

EQ {T}

By: Unfold `equivalence` 0 THEN DiscreteEq 2 THEN AbSetMemEqTypeCD

Generated subgoals:

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

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

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

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

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

About:

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

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