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* T:Type, eq:{T }, L,M:T List. L(eq)M Type | [is_intersection_wf] |
| Thm* a:T, R,S:T List, b:T. [a] = (R @ (b.S)) a = b | [singelton_append_equals_lemma] |
Thm* P:(T  Prop), 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* 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* 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=}, 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,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* L1,L2,L3:T List. (L1 @ (L2 @ L3)) = ((L1 @ L2) @ L3) | [append_associative] |
| 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* T:Type, L,M:T List, eq:(TT). (eq)(L,M) | [apply_wf_sublist_2] |
| Thm* T:Type, L,M:T List, eq:(TT). (eq)(L,M) | [apply_sublist_2_wf] |
| 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] |
| Thm* T:Type, eq:{T}, L1,L2:T List. L1(eq)L2 Type | [sublist_wf2] |
| Thm* T:Type, eq:{T=}, L1,L2:T List. L1(eq)L2 Type | [sublist_wf1] |
| Thm* T:Type, eq:(TT), L1,L2:T List. L1(eq)L2 Type | [sublist_wf] |
| Thm* L:T List. (L @ nil) = L | [append_nil_right_identity] |
| 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}, 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:(TT), L1,L2:T List, x:T. disjoint(eq;(x.L1);L2) disjoint(eq;L1;L2) | [disjoint_tail] |
| Thm* eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2)) | [decidable__disjoint] |
| 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* T:Type, P:(T), L:T List. xL.P(x) | [list_exists_2_wf] |
| Thm* P:(T), L:T List. xL.P(x) xL.P(x) | [list_all_2_all] |
| 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* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x)) | [decidable__list_exists] |
| Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type | [list_exists_wf] |
| 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* 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* T:Type, P:(T), L:T List. xL.P(x) | [list_all_2_wf] |
| Thm* L:T List, x:T. x(x.L).False False | [list_all_of_false_false] |
| 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* T:Type, P:(TType). xnil.P(x) Type | [list_all_wf_nil] |
| Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type | [list_all_wf] |
| 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] |
| Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L | [is_member_wf] |
| Thm* T:Type, eq:(TT), u:T. u(eq) nil | [is_member_wf_nil] |
| Thm* T:Type, f:(T), L:T List. filter(f;L) {x:T| f(x) } List | [filter_wf_subtype] |
| Thm* T:Type, f:(T), L:T List. filter(f;L) T List | [filter_wf] |
| Thm* T:Type, eq:(TT), x:T, L:T List. remove(eq;x;L) T List | [remove_wf] |
| 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] |
| Thm* Discrete{T} Discrete{(T List)} | [discrete__list] |
Thm* T:Type, L:T List. ||L||  | [length_wf_nat] |
Thm* L:T List. | |(L)0 | [list_length_non_negative] |
Thm* T:Type, L:T List. ||(L)  | [apply_wf_list_length_int] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length_nat] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length] |
| Thm* T:Type. || (T List) | [list_length_wf_int] |
| Thm* T:Type. || (T List) | [list_length_wf_nat] |