is mentioned by

Thm* eq:{T}, L:T List. L nil (x:T. x(eq) L)

[non_nil_is_member]

In prior sections: int 1 bool 1 int 2