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

At: remove is member lemma 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)

u:T, L:T List, v:T. v(eq) remove(eq;u;L) v(eq) L

By: UnivCD

Generated subgoal:

17. u: T
8. L: T List
9. v: T
10. v(eq) remove(eq;u;L)
v(eq) L

About:
listboolassertapplyfunctionuniversememberimpliesall

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