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

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

At: list exists is member lemma 2 2 1 2

1. T: Type
2. eq: TT
3. (x,y:T. eq(x,y) x = y) & 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. yv.P(y)

x:T. x(eq) (u.v) & P(x)

By: RenameVar `x' 9 THEN Witness8 x

Generated subgoal:

1 8. x: yv.P(y)
9. x:T. x(eq) v & P(x)
x:T. x(eq) (u.v) & P(x)

About:

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