Nuprl - Pf list exists exists 1 2 2 1 1 3 1 1 1 2 1 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

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. 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

By: IfThenElseCases 11

Generated subgoals:

1 11. eq(x,u) = true
12. true
13. P(x)
14. x = u
15. eq(x,u) x = u
x(eq) v

2 11. eq(x,u) = false
12. x(eq) v
13. P(x)
14. x = u
15. eq(x,u) x = u
x(eq) v

About:

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