eq:{T=
}, L:T List, x:T. x(
eq) L 
(
M,N:T List. L = (M @ (x.N)) & remove(eq;x;L) = (M @ N))P:
. P 
P = true| Theorem | Name | ||
| Thm* eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N)) & remove(eq;x;L) = (M @ N)) | [is_member_remove_lemma] | ||
| cites | |||
| Thm* P:. P P = true | [assert_iff_btrue] |