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

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

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

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

u(eq) v

By: Witness4 u THEN With u (Analyze -1)

Generated subgoal:

1 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

About:

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