Nuprl - Pf sublist transitivity 1 1 1 1 1 1 1

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

At: sublist transitivity 1 1 1 1 1 1 1

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

z(eq) L3

By: Inst Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [T;f;z.z(eq) L2;L1] THEN ReduceSOAps -1 THEN Analyze -1 THEN Thin -1 THEN Inst Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [T;f;z.z(eq) L3;L2] THEN ReduceSOAps -1 THEN Analyze -1 THEN Thin -1

Generated subgoal:

1 18. xL1.x(eq) L2 (z:T. z(f) L1 z(eq) L2)
19. xL2.x(eq) L3 (z:T. z(f) L2 z(eq) L3)
z(eq) L3

About:

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