Nuprl - Pf sublist functionality wrt id id list iso

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

At: sublist functionality wrt id id list iso

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

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

Generated subgoal:

1 1. 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. L3: T List
15. L4: T List
16. Discrete{T}
17. eq1 = eq2 {T}
18. L1 = L2
19. L3(~eq1)L4
L1(eq2)L3 L2(eq2)L4

About:

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