Nuprl - Pf append functionality wrt sublist 1 1 2

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

At: append functionality wrt sublist 1 1 2

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. L3(eq)L4
13. u: T
14. v: T List
15. v(eq)L2 (v @ L3)(eq)(L2 @ L4)

(u.v)(eq)L2 ((u.v) @ L3)(eq)(L2 @ L4)

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

Generated subgoals:

1 16. u(eq) L2
17. v(eq)L2
u(eq) (L2 @ L4)

2 16. u(eq) L2
17. v(eq)L2
(v @ L3)(eq)(L2 @ L4)

About:

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