is mentioned by

Thm* eq:{T}, L:T List. ||L||1 hd(L)(eq) L	[hd_is_member_lemma]
Thm* L:T List. ||(L)0	[list_length_non_negative]

In prior sections: int 2 list 1