Nuprl - Pf list exists is member lemma 2 2 1 1 1 1 1 1 1

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

At: list exists is member lemma 2 2 1 1 1 1 1 1 1

1. T: Type
2. eq: TT
3. eq TT
4. P: TProp
5. L: T List
6. u: T
7. v: T List
8. yv.P(y) (x:T. x(eq) v & P(x))
9. P(u)
10. eq(u,u) u = u
11. (eq(u,u)) (u = u)
12. u = u
13. eq(u,u)

if eq(u,u) true else u(eq) v fi

By: OnHyps [12;11;10] (i.Thin i) THEN FwdThru Thm* P:. P P = true [-1]

Generated subgoal:

1 10. eq(u,u)
11. eq(u,u) = true
if eq(u,u) true else u(eq) v fi

About:

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