is mentioned by

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_sublist]
Thm* Discrete{T} (eq:{T}, L,M:T List. (L @ M)(eq)(M @ L))	[append_commutes_under_sublist]
Thm* eq:{T=}, L:T List. L(eq)nil L = nil	[sublist_of_nil_iff_nil]
Thm* L,M:T List, eq:{T=}. L(eq)M (eq)(L,M)	[sublist_iff_assert_sublist_2_x]
Thm* Discrete{T} (eq:{T}, L,M:T List. L(eq)M (eq)(L,M))	[sublist_iff_assert_sublist_2]
Thm* eq:{T=}, x:T, L,M:T List. x(eq) L L(eq)M x(eq) M	[is_member_sublist_lemma]
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* eq:{T=}, L:T List. L(eq)L	[sublist_reflexive]
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* eq:{T=}, u:T, v:T List. v(eq)(u.v)	[sublist_tail1]
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]
Def L1(~eq)L2 == L1(eq)L2 & L2(eq)L1	[list_iso]