Nuprl - Pf remove is member 1 1

(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))

x(eq) (u.v)

By: AbReduce 0 THEN IfThenElseCases 0

Generated subgoals:

1 10. eq(x,u) = true
true

2 10. 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` `true`
2	10. `eq(x,u) = false` `x(eq) v`