is mentioned by

Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) L P(x) x(eq) filter((x.P(x));L)	[filter_is_member_lemma]
Thm* eq:{T=}, P:(T), L:T List, x:T. x(eq) filter((x.P(x));L) P(x)	[is_member_filter_lemma]
Thm* T:Type, L,M:T List, eq:(TT). (eq)(L,M)	[apply_wf_sublist_2]
Thm* T:Type, L,M:T List, eq:(TT). (eq)(L,M)	[apply_sublist_2_wf]
Thm* T:Type, eq:(TT), L1,L2:T List. L1(eq)L2 Type	[sublist_wf]
Thm* T:Type, eq:{T}, L,M:T List. disjoint(eq;L;M)	[disjoint2_wf]
Thm* eq:(TT), L1,L2:T List, x:T. disjoint(eq;(x.L1);L2) disjoint(eq;L1;L2)	[disjoint_tail]
Thm* eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2))	[decidable__disjoint]
Thm* T:Type, P:(T), L:T List. xL.P(x)	[list_exists_2_wf]
Thm* P:(T), L:T List. xL.P(x) xL.P(x)	[list_all_2_all]
Thm* eq:(TT), L:T List. xL.x(eq) nil nil = L	[list_all_is_member_nil_lemma]
Thm* L:T List, P:(T). xL.P(x) xL.P(x)	[list_all_iff_assert_list_all_2]
Thm* eq:{T}, P:(T), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x))	[not_list_all_2_implies_exists_not]
Thm* T:Type, P:(T), L:T List. xL.P(x)	[list_all_2_wf]
Thm* eq:(TT), x:T, L:T List. Dec(x(eq) L)	[decidable__is_member]
Thm* eq:(TT), x:T, L:T List. SqStable(x(eq) L)	[sq_stable__is_member]
Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L	[is_member_wf]
Thm* T:Type, eq:(TT), u:T. u(eq) nil	[is_member_wf_nil]
Thm* T:Type, f:(T), L:T List. filter(f;L) {x:T| f(x) } List	[filter_wf_subtype]
Thm* T:Type, f:(T), L:T List. filter(f;L) T List	[filter_wf]
Thm* T:Type, eq:(TT), x:T, L:T List. remove(eq;x;L) T List	[remove_wf]
Thm* L:T List. null(L) = false (h:T, t:T List. L = h.t)	[null_false_lemma]
Thm* L:T List. null(L) = true L = nil	[null_true_lemma]

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