is mentioned by

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* P:(T), L:T List. xL.P(x) xL.P(x)	[list_all_2_all]
Thm* eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x))	[list_all_all]
Thm* eq:(TT), L:T List. xL.x(eq) nil nil = L	[list_all_is_member_nil_lemma]
Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z))	[list_all_is_member_lemma]
Thm* L:T List, P:(T). xL.P(x) xL.P(x)	[list_all_iff_assert_list_all_2]
Thm* L:T List, x:T. x(x.L).False False	[list_all_of_false_false]
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]
Def L1(eq)L2 == xL1.x(eq) L2	[sublist]
Def disjoint(eq;L1;L2) == xL1.x(eq) L2	[disjoint]