Nuprl - Pf equivalence properties

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

T:Type, f:{T}. (x,y,z:T. f(x,y) f(y,z) f(x,z)) & (x,y:T. f(x,y) f(y,x)) & (x:T. f(x,x)) & f TT

By: ProvePropertiesLemma

Generated subgoals:

1 1. T: Type
2. f: TT
3. x:T. f(x,x)
4. x,y:T. f(x,y) f(y,x)
5. x,y,z:T. f(x,y) f(y,z) f(x,z)
6. x: T
7. y: T
8. z: T
9. f(x,y)
10. f(y,z)
f(x,z)

2 1. T: Type
2. f: TT
3. x:T. f(x,x)
4. x,y:T. f(x,y) f(y,x)
5. x,y,z:T. f(x,y) f(y,z) f(x,z)
6. x: T
7. y: T
8. f(x,y)
f(y,x)

3 1. T: Type
2. f: TT
3. x:T. f(x,x)
4. x,y:T. f(x,y) f(y,x)
5. x,y,z:T. f(x,y) f(y,z) f(x,z)
6. x: T
7. y: T
8. f(y,x)
f(x,y)

4 1. T: Type
2. f: TT
3. x:T. f(x,x)
4. x,y:T. f(x,y) f(y,x)
5. x,y,z:T. f(x,y) f(y,z) f(x,z)
6. x: T
f(x,x)

About:

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

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