Theoremslength_eq, refl, smash, snoc, snoc_snoc_swap, trans, eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero, eq_snoc_eraseLast, exists_last_eq_snoc_equivalent, ext, ext_iff, head_le, head_le_of_mem, inj, injective, isMaximal_eraseLast_last, jordan_holder, last_eraseLast_le, le_last, le_last_of_mem, length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero, length_pos_of_head_eq_head_of_last_eq_last_of_length_pos, lt_last_of_mem_eraseLast, lt_succ, mem_eraseLast, mem_eraseLast_of_ne_of_mem, snoc_eraseLast_last, strictMono, toList_nodup, toList_sorted, total, iso_refl, isMaximal_inf_left_of_isMaximal_sup, isMaximal_inf_right_of_isMaximal_sup, isMaximal_of_eq_inf, iso_symm, iso_trans, lt_of_isMaximal, second_iso, second_iso_of_eq, sup_eq_of_isMaximal | 41 |