is mentioned by

Thm* L:T List. null(L) = false (h:T, t:T List. L = h.t)	[null_false_lemma]
Def disjoint(eq;L;M) == (letrec disjoint2 L = (Case of L; nil true ; h.t if h(eq) M false else disjoint2(t) fi) ) (L)	[disjoint2]
Def xL.P(x) == (letrec exists L = (Case of L; nil false ; h.t P(h) exists(t)) ) (L)	[list_exists_2]
Def x(eq) L == (letrec is_member x eq L = (Case of L; nil false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L)	[is_member]

In prior sections: bool 1 bool 2 jlc list 1