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

At: list iso transitivity 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
By: OnHyps [24;23;0] (i.UnfoldTopAb i THEN Analyze i)
Generated subgoals:

123. L1(eq1)L2
24. L2(eq1)L1
25. L2(eq2)L3
26. L3(eq2)L2
L1(eq3)L3
223. L1(eq1)L2
24. L2(eq1)L1
25. L2(eq2)L3
26. L3(eq2)L2
L3(eq3)L1

About:
listboolassertapplyfunctionuniverseequalmemberimpliesall

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