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