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* a:T, R,S:T List, b:T. [a] = (R @ (b.S)) a = b | [singelton_append_equals_lemma] |
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* (x,y:T. Dec(x = y)) (L,M:T List. Dec(L = M)) | [decidable__equal_list] |
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* Discrete{T} (eq:{T}, L,M:T List. L = M L(~eq)M) | [list_iso_weakening_wrt_identity] |
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* 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: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* 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* 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. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M) | [not_disjoint_is_member_lemma] |
| Thm* eq:(TT), L1,L2:T List, x:T. disjoint(eq;(x.L1);L2) disjoint(eq;L1;L2) | [disjoint_tail] |
| 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}, x,y:T, L:T List. x(eq) remove(eq;y;L) x(eq) L | [remove_is_member] |
| Thm* P:(T), L:T List. xL.P(x) xL.P(x) | [list_all_2_all] |
| Thm* eq:{T=}, P:(TProp), x:T, L:T List. x(eq) L P(x) yL.P(y) | [list_exists_is_member_lemma1] |
| Thm* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x)) | [decidable__list_exists] |
| 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* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x)) | [decidable__list_all] |
| Thm* P:(TProp), L:T List. (x:T. SqStable(P(x))) SqStable(xL.P(x)) | [sq_stable__list_all] |
| Thm* P:(TProp), L:T List, x:T. x(x.L).P(x) xL.P(x) | [list_all_tail] |
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* Discrete{T} Discrete{(T List)} | [discrete__list] |