is mentioned by

Thm* eq:{T=}, L,M:T List. L(eq)M (x:{x:T| x(eq) L }. x(eq) M)	[is_intersection_implies_exists_element]
Thm* eq:{T}, u:T, L:T List, v:T. v(eq) remove(eq;u;L) v(eq) L	[remove_is_member_lemma]
Thm* eq:{T=}, x,y:T, L:T List. x(eq) L eq(x,y) x(eq) remove(eq;y;L)	[not_is_member_remove_lemma]
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* eq:{T}, x:T, L:T List. x(eq) L (y:T. x(eq) (y.L))	[is_member_tail]
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=}, u:T, L:T List. u(eq) L (v:T, M:T List. L = v.M)	[is_member_non_nil]
Thm* eq:{T=}, L:T List, x:T. (M,N:T List. L = (M @ (x.N))) x(eq) L	[append_is_member_lemma]
Thm* eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) (M @ L)	[append_commutes_under_is_member]
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]
Thm* eq:{T}, L:T List, x:T. x(eq) L (M,N:T List, y:T. eq(x,y) & L = (M @ (y.N)))	[is_member_append_lemma1]
Thm* eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N)))	[is_member_append_lemma]
Thm* eq:{T=}, x:T, L,M:T List. x(eq) L L(eq)M x(eq) M	[is_member_sublist_lemma]
Thm* EQ:{T=}, eq:{T}, L,M:T List. L(eq)M (z:T. z(EQ) L z(eq) M)	[sublist_list_all_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}, x,y:T, L:T List. x(eq) remove(eq;y;L) x(eq) L	[remove_is_member]
Thm* eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x))	[list_all_all]
Thm* eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x))	[list_exists_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* 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* 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* eq:{T}, t:T, L:T List. t(eq) (t.L)	[is_member_cons]
Thm* eq:{T}, L:T List. L nil (x:T. x(eq) L)	[non_nil_is_member]
Thm* eq:{T}, L:T List. ||L||1 hd(L)(eq) L	[hd_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]
Thm* eq:{T=}, u:T, L:T List. u(eq) L (f:{T}. u(f) L)	[is_member_equalities_lemma]
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]
Def L(eq)M == xL.x(eq) M	[is_intersection]
Def (eq)(L,M) == xL.x(eq) M	[sublist_2]
Def L1(eq)L2 == xL1.x(eq) L2	[sublist]
Def disjoint(eq;L;M) == (letrec disjoint2 L = (Case of L; nil true ; h.t if h(eq) M false else disjoint2(t) fi) ) (L)	[disjoint2]
Def disjoint(eq;L1;L2) == xL1.x(eq) L2	[disjoint]