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

At: remove is member 1 1 1
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))
10. eq(x,u) = true

true
By: BackThru Thm* P:. P P = true
Generated subgoals:

None

About:
listconsboolbtrueassertapplyuniverseequalimplies

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