is mentioned by

Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x)	[list_exists_append_lemma]
Thm* eq:{T}, x:T, L,M:T List. x(eq) (L @ M) x(eq) L x(eq) M	[is_member_append_disjunction_lemma]
Thm* eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) L x(eq) M	[is_member_of_append_lemma]
Def xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L)	[list_exists]

In prior sections: core bool 1 core 3 jlc int 2 list 1