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

At: remove is member lemma 1 1 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. v(eq) remove(eq;u;L)

v(eq) L

By: ListInd 8

Generated subgoals:

1 v(eq) remove(eq;u;nil) v(eq) nil
210. u1: T
11. v1: T List
12. v(eq) remove(eq;u;v1) v(eq) v1
v(eq) remove(eq;u;(u1.v1)) v(eq) (u1.v1)

About:
listconsnilboolassertapplyfunctionuniversememberimpliesall

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