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

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

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

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. x: T
12. if eq(x,u) true else x(eq) v fi
13. P(x)
14. x = u

x(eq) v

By: Witness4 x 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. x: T
11. if eq(x,u) true else x(eq) v fi
12. P(x)
13. x = u
14. eq(x,u) x = u
x(eq) v

About:

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