is mentioned by

Thm* P:(TProp), L:T List. xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N)))	[list_exists_is_member_append_lemma]
Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) & xM.P(x)	[list_all_append_lemma]
Thm* eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N)) & remove(eq;x;L) = (M @ N))	[is_member_remove_lemma]
Thm* eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M)	[not_disjoint_is_member_lemma]
Thm* eq:{T=}, P:(TProp), L:T List. (x:T. x(eq) L & P(x)) yL.P(y)	[list_exists_is_member_lemma]
Thm* equiv:{T}, eq:{T=}, u:T, L:T List. u(equiv) L (v:T. equiv(u,v) & v(eq) L)	[is_member_equality_strengthening_lemma]
Def L1(~eq)L2 == L1(eq)L2 & L2(eq)L1	[list_iso]
Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L)	[list_all]

In prior sections: core int 1 bool 1 discrete jlc core 3 jlc int 2 fun 1