Nuprl - list 3 jlc LEMMAs for remove is member

Theorem	Name
		Thm* eq:{T}, x,y:T, L:T List. x(eq) remove(eq;y;L) x(eq) L	[remove_is_member]
cites
		Thm* P:. P P = true	[assert_iff_btrue]