Nuprl - Pf list exists exists 1 2 1 1 1 1 1 2 1

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

At: list exists exists 1 2 1 1 1 1 1 2 1

1. T: Type
2. eq: {T=}
3. eq TT
4. P: TType
5. L: T List
6. u: T
7. v: T List
8. xv.P(x) (x:{x:T| x(eq) v }. P(x))
9. xv.P(x) (x:{x:T| x(eq) v }. P(x))
10. P(u)
11. eq(u,u) = false
12. eq(u,u) u = u

u(eq) v

By: FwdThru Thm* P:. P P = false [-2]

Generated subgoal:

1 12. eq(u,u) u = u
13. (eq(u,u)) (u = u)
14. eq(u,u)
u(eq) v

About:

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