is mentioned by

Thm* P:(TProp), L:T List. xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N)))	[list_exists_is_member_append_lemma]
Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x)	[list_exists_append_lemma]
Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) & xM.P(x)	[list_all_append_lemma]
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* eq:{T}, L,M:T List. L(~eq)M M(~eq)L	[list_iso_commutative]
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. 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=}, 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) disjoint(eq;L;M)	[disjoint_iff_assert_disjoint2]
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* 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), 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* 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* 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: core well fnd int 1 bool 1 bool 2 jlc discrete jlc core 3 jlc fun 1 int 2 list 1