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

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

At: sublist transitivity 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 2 1 1 1 2

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. f: {T=}
12. f TT
13. x,y:T. f(x,y) x = y
14. z: T
15. z(f) L1
16. u: T
17. v: T List
18. eq(z,u) = true
19. True
20. f(u,u)
21. f(u,u) = true
22. u1: T
23. v1: T List
24. u(eq) v1 z(eq) v1

u(eq) (u1.v1) z(eq) (u1.v1)

By: Rewrite (HigherC is_member_unrollC) 0

Generated subgoal:

1 if eq(u,u1) true else u(eq) v1 fi if eq(z,u1) true else z(eq) v1 fi

About:

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