Nuprl - Pf list iso transitivity

(4steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

T:Type. Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L2(~eq2)L3 L1(~eq3)L3)

By: Analyze 0 THEN Analyze 0 THEN Analyze 0 THEN Equivalence -1 THEN Analyze 0 THEN Equivalence -1 THEN Analyze 0 THEN Equivalence -1 THEN UnivCD

Generated subgoal:

1 1. T: Type
2. Discrete{T}
3. eq1: {T}
4. eq1 TT
5. x:T. eq1(x,x)
6. x,y:T. eq1(x,y) eq1(y,x)
7. x,y,z:T. eq1(x,y) eq1(y,z) eq1(x,z)
8. eq2: {T}
9. eq2 TT
10. x:T. eq2(x,x)
11. x,y:T. eq2(x,y) eq2(y,x)
12. x,y,z:T. eq2(x,y) eq2(y,z) eq2(x,z)
13. eq3: {T}
14. eq3 TT
15. x:T. eq3(x,x)
16. x,y:T. eq3(x,y) eq3(y,x)
17. x,y,z:T. eq3(x,y) eq3(y,z) eq3(x,z)
18. L1: T List
19. L2: T List
20. L3: T List
21. eq1 = eq2 {T}
22. eq2 = eq3 {T}
23. L1(~eq1)L2
24. L2(~eq2)L3
L1(~eq3)L3

About:

(4steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc