Nuprl - Pf not is member remove lemma 1 1 1

(14steps) 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. eq(x,y)
7. u: T
8. v: T List
9. x(eq) v x(eq) remove(eq;y;v)
10. if eq(x,u) true else x(eq) v fi
11. eq(y,u) = true

x(eq) v

By: IfThenElseCases -2

Generated subgoals:

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

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

About:

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

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