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

At: list iso transitivity 1 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(eq1)L1
25. L2(eq2)L3
26. L3(eq2)L2

L1(eq3)L3
By: Using [`L2',L2;`eq2',eq2;`eq1',eq1] (BackThru Thm* Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(eq1)L2 L2(eq2)L3 L1(eq3)L3))
Generated subgoals:

None

About:
listboolassertapplyfunctionuniverseequalmemberimpliesall

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