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

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

At: sublist functionality wrt id list iso id 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(~eq)L2
13. L3 = L4

L1(eq)L3 L2(eq)L4

By: HypSubst 13 0 THEN UnfoldTopAb 12 THEN UnfoldTopAb 12 THEN Analyze 12 THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 12. L1(eq)L2
13. L2(eq)L1
14. L3 = L4
15. L1(eq)L4
L2(eq)L4

2 12. L1(eq)L2
13. L2(eq)L1
14. L3 = L4
15. L2(eq)L4
L1(eq)L4

About:

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