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.

changed the description

changed the description

mentioned in merge request !441 (merged)

Wow I didn't realize we could have half a dozen lemmas like list_eq_prefix_length, for maps and sets and various relations on lists. Nice!

resolved all threads

added 1 commit

• c1caa660 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

Thanks. Going to merge!

enabled an automatic merge when the pipeline for c1caa660 succeeds

@iris-users This is a potential breaking change:

• Add Permutation_submseteq_length to replace Permutation_alt, submseteq_Permutation_length_le and submseteq_Permutation_length_eq.
• Remove map_to_list_length (which seemed to be an unneeded auxiliary lemma); use map_subset_size instead.

aborted the automatic merge because source branch was updated

added 2 commits

• 83142b07 - Get rid of bi-implications.
• 168d9be7 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 40 commits

• 168d9be7...32e33c9d - 31 commits from branch master
• f6c51d9c - Add `subset_proper`.
• 0a0aa08b - Add `list_eq_prefix_length` and `list_eq_suffix_length`.
• 3476f4ae - Add `Permutation_submseteq_length` to replace `Permutation_alt`,...
• 5d722b20 - Add `set_equiv_subseteq_size` and `set_eq_subseteq_size`.
• 25cb389d - Add `map_eq_subseteq_size`, `map_subseteq_size`, `map_subset_size`.
• ab94b79a - Simplify proofs of map induction principles; remove `map_to_list_length`.
• fa9f81a2 - Add `dom_subseteq_size`, `dom_subset_size`, `map_eq_subseteq_dom`.
• 0bfc9671 - Get rid of bi-implications.
• c9077e52 - CHANGELOG.

Compare with previous version

added 2 commits

• 3134139c - Get rid of bi-implications.
• a8f4a69c - CHANGELOG.

Compare with previous version

added 1 commit

• 8d06dc6e - CHANGELOG.

Compare with previous version

resolved all threads

merged