is mentioned by

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]