Nuprl - Pf sublist functionality wrt id id list iso 1 1 1

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

At: sublist functionality wrt id id list iso 1 1 1

1. T: Type
2. L1: T List
3. L2: T List
4. eq: {T}
5. eq TT
6. x:T. eq(x,x)
7. x,y:T. eq(x,y) eq(y,x)
8. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
9. L3: T List
10. L4: T List
11. Discrete{T}
12. L1 = L2
13. L3(eq)L4
14. L4(eq)L3
15. L2(eq)L3

L2(eq)L4

By: Inst 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) [T;eq;eq;eq;L2;L1;L3] THEN Inst 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) [T;eq;eq;eq;L2;L3;L4]

Generated subgoals:

1 16. L2(eq)L4
L2(eq)L1

2 16. L2(eq)L4
L1(eq)L3

3 16. L2(eq)L3
17. L2(eq)L4
L2(eq)L4

About:

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

1	16. `L2(eq)L4` `L2(eq)L1`
2	16. `L2(eq)L4` `L1(eq)L3`
3	16. `L2(eq)L3` 17. `L2(eq)L4` `L2(eq)L4`