Nuprl - Pf remove is member 1 1 2

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

1. T: Type
2. eq: {T}
3. x: T
4. y: T
5. L: T List
6. u: T
7. v: T List
8. x(eq) remove(eq;y;v) x(eq) v
9. x(eq) remove(eq;y;(u.v))
10. eq(x,u) = false

x(eq) v

By: AbReduce -2 THEN IfThenElseCases -2

Generated subgoals:

1 9. eq(y,u) = true
10. x(eq) v
11. eq(x,u) = false
x(eq) v

2 9. eq(y,u) = false
10. x(eq) (u.remove(eq;y;v))
11. eq(x,u) = false
x(eq) v

About:

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

1	9. `eq(y,u) = true` 10. `x(eq) v` 11. `eq(x,u) = false` `x(eq) v`
2	9. `eq(y,u) = false` 10. `x(eq) (u.remove(eq;y;v))` 11. `eq(x,u) = false` `x(eq) v`