Theoremsnodup, append, attach, concat, cons, diff, diff_eq_filter, disjoint, erase_get, erase_getElem, filter, filterMap, getElem_inj_iff, get_inj_iff, injective_get, insert, inter, map, map_on, map_update, mem_diff_iff, mergeSort, ne_singleton_iff, notMem, of_append_left, of_append_right, of_attach, of_cons, of_map, pairwise_of_forall_ne, pmap, product, sigma, take_eq_filter_mem, union, nodup, nodup, count_eq_of_nodup, count_eq_one_of_mem, disjoint_of_nodup_append, getElem_bijective_iff, get_bijective_iff, get_idxOf, idxOf_getElem, inj_on_of_nodup_map, nodup_append', nodup_append_comm, nodup_attach, nodup_concat, nodup_flatMap, nodup_flatten, nodup_iff_count_eq_one, nodup_iff_count_le_one, nodup_iff_getElem?_ne_getElem?, nodup_iff_injective_get, nodup_iff_injective_getElem, nodup_iff_sublist, nodup_map_iff, nodup_map_iff_inj_on, nodup_mergeSort, nodup_middle, nodup_reverse, nodup_singleton, nodup_tail_reverse, not_nodup_cons_of_mem, not_nodup_of_get_eq_of_ne, not_nodup_pair, rel_nodup, toList_nodup | 69 |