is mentioned by

Thm* L:T List. null(L) = true L = nil	[null_true_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 all L = (Case of L; nil true ; h.t P(h)(all(t))) ) (L)	[list_all_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