Nuprl - Pf sublist transitivity 1

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

1. T: Type
2. Discrete{T}
3. eq1: {T}
4. eq1 TT
5. x:T. eq1(x,x)
6. x,y:T. eq1(x,y) eq1(y,x)
7. x,y,z:T. eq1(x,y) eq1(y,z) eq1(x,z)
8. eq2: {T}
9. eq2 TT
10. x:T. eq2(x,x)
11. x,y:T. eq2(x,y) eq2(y,x)
12. x,y,z:T. eq2(x,y) eq2(y,z) eq2(x,z)
13. eq3: {T}
14. eq3 TT
15. x:T. eq3(x,x)
16. x,y:T. eq3(x,y) eq3(y,x)
17. x,y,z:T. eq3(x,y) eq3(y,z) eq3(x,z)
18. L1: T List
19. L2: T List
20. L3: T List
21. eq1 = eq2 {T}
22. eq2 = eq3 {T}
23. L1(eq1)L2
24. L2(eq2)L3

L1(eq3)L3

By: HypSubst 21 23 THENA Equivalence -1 THEN HypSubst 22 23 THENA Equivalence -1 THEN HypSubst 22 24 THENA Equivalence -1

Generated subgoal:

1 23. L1(eq3)L2
24. L2(eq3)L3
L1(eq3)L3

About:

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