is mentioned by

Thm* L:T List. null(L) = false (h:T, t:T List. L = h.t)	[null_false_lemma]
Thm* L:T List. null(L) = true L = nil	[null_true_lemma]

In prior sections: list 1