Nuprl - Pf not is member remove lemma 1 1 1 1 1 1

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

At: not is member remove lemma 1 1 1 1 1 1

1. T: Type
2. eq: {T=}
3. x: T
4. y: T
5. L: T List
6. eq(x,y)
7. u: T
8. v: T List
9. x(eq) v x(eq) remove(eq;y;v)
10. eq(x,u) = true
11. true
12. eq(y,u) = true
13. eq(y,u)
14. eq(x,u)
15. x = u
16. y = u

x(eq) v

By: Analyze 6

Generated subgoal:

1 6. u: T
7. v: T List
8. x(eq) v x(eq) remove(eq;y;v)
9. eq(x,u) = true
10. true
11. eq(y,u) = true
12. eq(y,u)
13. eq(x,u)
14. x = u
15. y = u
eq(x,y)

About:

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