# Various tweaks to lists, maps, sets

While reviewing !442 (merged) and !441 (merged) I ran into a bunch of stuff that should be improved:

- Add
`subset_proper`

. - Add
`list_eq_prefix_length`

and`list_eq_suffix_length`

.**The version for**`prefix`

is also part of !441 (merged), but the version for`suffix`

was missing there. - Add
`set_equiv_subseteq_size`

and`set_eq_subseteq_size`

.**Similar to the prior lemmas, but now for set equality. These are not part of !441 (merged) and !442 (merged).** - Add
`dom_subseteq_size`

,`dom_subset_size`

,`map_eq_subseteq_dom`

.**The last lemma is part of !442 (merged), but the version in this MR is stronger since it requires**`Set_`

instead of`FinSet`

) - Add
`map_eq_subseteq_size`

,`map_subseteq_size`

,`map_subset_size`

.**These lemmas are also part of !442 (merged), but the statement and naming are made consistent with similar lemmas for sets, and the proof have been shortened.** - Add
`Permutation_submseteq_length`

to replace`Permutation_alt`

,`submseteq_Permutation_length_le`

and`submseteq_Permutation_length_eq`

.**This makes the statement and naming consistent with the new lemmas for prefix/suffix/sets/maps** - Simplify proofs of map induction principles; remove
`map_to_list_length`

.

Edited by Robbert Krebbers