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

At: remove is member lemma

T:Type, eq:{T}, u:T, L:T List, v:T. v(eq) remove(eq;u;L) v(eq) L
By:
Analyze 0
THEN
Analyze 0
Generated subgoal:

11. T: Type
2. eq: {T}
u:T, L:T List, v:T. v(eq) remove(eq;u;L) v(eq) L

About:
listassertuniverseimpliesall

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