list_eq_suffix_length. The version for
prefixis also part of !441 (merged), but the version for
suffixwas missing there.
set_eq_subseteq_size. Similar to the prior lemmas, but now for set equality. These are not part of !441 (merged) and !442 (merged).
map_eq_subseteq_dom. The last lemma is part of !442 (merged), but the version in this MR is stronger since it requires
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.
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