is mentioned by

Thm* T:Type, eq:{T}, L,M:T List. L(eq)M Type	[is_intersection_wf]
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}, L,M:T List. Dec(L(~eq)M)	[decidable__list_iso]
Thm* Discrete{T} (eq:{T}, L,M:T List. L(~eq)M (~eq)(L,M))	[list_iso_iff_assert_list_iso_2]
Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1(~eq3)L3 L2(~eq3)L4)	[list_iso_functionality_wrt_id_list_iso_list_iso]
Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(~eq2)L3 L2(~eq2)L4)	[list_iso_functionality_wrt_id_list_iso_id]
Thm* L1,L2:T List, eq1,eq2,eq3,eq4:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 eq3 = eq4 L1(~eq1)L2 L3(~eq2)L4 (L1(eq3)L3 L2(eq4)L4)	[sublist_functionality_wrt_id_list_iso_list_iso]
Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1 = L2 L3(~eq1)L4 (L1(eq2)L3 L2(eq2)L4)	[sublist_functionality_wrt_id_id_list_iso]
Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(eq2)L3 L2(eq2)L4)	[sublist_functionality_wrt_id_list_iso_id]
Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1 @ L3)(~eq3)(L2 @ L4)	[append_functionality_wrt_list_iso]
Thm* Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L2(~eq2)L3 L1(~eq3)L3)	[list_iso_transitivity]
Thm* Discrete{T} (eq1,eq2:{T}, L,M:T List. eq1 = eq2 L(~eq1)M M(~eq2)L)	[list_iso_inversion]
Thm* eq:{T}, L,M:T List. L(~eq)M M(~eq)L	[list_iso_commutative]
Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(~eq)M)	[list_iso_weakening_wrt_identity]
Thm* eq:{T}, x:T, L:T List. x(eq) L (y:T. x(eq) (y.L))	[is_member_tail]
Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(eq1)L2 L3(eq2)L4 (L1 @ L3)(eq3)(L2 @ L4)	[append_functionality_wrt_sublist]
Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(~eq)(M @ L))	[append_commutes_under_list_iso]
Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(eq)(M @ L))	[append_commutes_under_sublist]
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* Discrete{T} (eq:{T}, L,M:T List. L(eq)M (eq)(L,M))	[sublist_iff_assert_sublist_2]
Thm* Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(eq1)L2 L2(eq2)L3 L1(eq3)L3)	[sublist_transitivity]
Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M)	[sublist_weakening_wrt_identity]
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* Discrete{T} (eq:{T}, u:T, v:T List. v(eq)(u.v))	[sublist_tail]
Thm* eq:{T}, L,M:T List. Dec(L(eq)M)	[decidable__sublist]
Thm* T:Type, eq:{T}, L1,L2:T List. L1(eq)L2 Type	[sublist_wf2]
Thm* eq:{T}, L,M:T List. disjoint(eq;L;M) disjoint(eq;L;M)	[disjoint_iff_assert_disjoint2]
Thm* T:Type, eq:{T}, L,M:T List. disjoint(eq;L;M)	[disjoint2_wf]
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:(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]

In prior sections: core 3 jlc