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

At: sublist functionality wrt id list iso list iso

T:Type, L1,L2:T List, eq1,eq2,eq3,eq4:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 eq3 = eq4 L1(~eq1)L2 L3(~eq2)L4 (L1(eq3)L3 L2(eq4)L4)
By:
RepeatFor 3 (Analyze 0)
THEN
RepeatFor 4 (Analyze 0 THEN Equivalence -1)
THEN
UnivCD
Generated subgoal:

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

About:
listuniverseequalimpliesall

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