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_exists_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* P:(TProp). (x:T. Dec(P(x))) (L:T List. xL.(P(x)) xL.P(x))	[not_list_all_not_iff_list_exists]
Thm* eq:{T=}, P:(TProp), x:T, L:T List. x(eq) L P(x) yL.P(y)	[list_exists_is_member_lemma1]
Thm* eq:{T=}, P:(TProp), L:T List. (x:T. x(eq) L & P(x)) yL.P(y)	[list_exists_is_member_lemma]
Thm* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x))	[decidable__list_exists]
Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type	[list_exists_wf]
Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z))	[list_all_is_member_lemma]
Thm* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x))	[decidable__list_all]
Thm* P:(TProp), L:T List. (x:T. SqStable(P(x))) SqStable(xL.P(x))	[sq_stable__list_all]
Thm* P:(TProp), L:T List, x:T. x(x.L).P(x) xL.P(x)	[list_all_tail]
Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type	[list_all_wf]

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