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

(17steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: remove is member lemma 1 1 1 2 1

1. T: Type
2. eq: {T}
3. eq TT
4. x:T. eq(x,x)
5. x,y:T. eq(x,y) eq(y,x)
6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7. u: T
8. L: T List
9. v: T
10. u1: T
11. v1: T List
12. v(eq) remove(eq;u;v1) v(eq) v1
13. v(eq) remove(eq;u;(u1.v1))

v(eq) (u1.v1)

By: Rewrite (HigherC remove_unrollC) -1 THEN IfThenElseCases -1

Generated subgoals:

1 13. eq(u,u1) = true
14. v(eq) v1
v(eq) (u1.v1)

2 13. eq(u,u1) = false
14. v(eq) (u1.remove(eq;u;v1))
v(eq) (u1.v1)

About:

(17steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc