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.