Nuprl - Pf remove is member 1 1 2 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. eq(y,u) = false
10. x(eq) (u.remove(eq;y;v))
11. eq(x,u) = false

x(eq) v

By: AbReduce -2 THEN IfThenElseCases -2

Generated subgoals:

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

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

About:

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

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