is mentioned by

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 xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L)	[list_exists]
Def xL.P(x) == (letrec all L = (Case of L; nil true ; h.t P(h)(all(t))) ) (L)	[list_all_2]
Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L)	[list_all]
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]
Def filter(f;L) == (letrec filter f L = (Case of L; nil nil ; h.t if f(h) h.filter(f,t) else filter(f,t) fi) ) (f,L)	[filter]
Def remove(eq;x;L) == (letrec remove eq x L = (Case of L; nil nil ; h.t if eq(x,h) t else h.remove(eq,x,t) fi) ) (eq,x,L)	[remove]
Def || == (letrec l L = (Case of L; nil 0 ; h.t 1+l(t)) )	[list_length]