Theoremsperm_iff_eq_of_sublist, coe_idxBij, countBefore_idxOfNth, diff, diff_left, diff_right, flatten_congr, getElem_idxBij_eq_getElem, getElem_idxBij_symm_eq_getElem, idxBij_idxBij_symm, idxBij_injective, idxBij_leftInverse_idxBij_symm, idxBij_rightInverse_idxBij_symm, idxBij_surjective, idxBij_symm_idxBij, idxBij_symm_leftInverse_idxBij, idxBij_symm_rightInverse_idxBij, insertP, inter, inter_left, inter_right, subperm, subperm_idxBij, subperm_left, subperm_right, union, union_left, union_right, coe_idxOrderInj, countBefore_idxOfNth, getElem_idxOrderInj_eq_getElem, idxOrderInj_inj, idxOrderInj_injective, subperm, subperm_idxOrderInj, antisymm, cons_left, cons_right, cons_self, countBefore_idxOfNth, countP_le, count_le, diff_right, erase, exists_of_length_lt, filter, getElem_idxInj_eq_getElem, idxInj_inj, idxInj_injective, length_le, perm_of_length_le, refl, subset, coe_idxInj, cons_subperm_of_not_mem_of_mem, erase_cons_subperm_cons_erase, erase_subperm, isSubperm_iff, nil_subperm, perm_ext_iff_of_nodup, perm_insertP, singleton_subperm_iff, subperm_append_diff_self_of_count_le, subperm_append_left, subperm_append_right, subperm_cons, subperm_cons_diff, subperm_cons_erase, subperm_ext_iff, subperm_nil, subperm_of_subset, subset_cons_diff | 72 |