miscellaneous map lemmas

some of these are from Perennial

added 30 commits

• 59ff9eae...469711e5 - 29 commits from branch master
• 4bbe48a0 - miscellaneous map lemmas

Compare with previous version

resolved all threads

Should be ready for review again.

added 1 commit

• 7a387a98 - miscellaneous map lemmas

Compare with previous version

added 1 commit

• 7b6d55bd - miscellaneous map lemmas

Compare with previous version

mentioned in merge request !455 (merged)

added 61 commits

• 7b6d55bd...20813c6c - 60 commits from branch master
• 3e937ea0 - miscellaneous map lemmas

Compare with previous version

added 1 commit

• 117074cc - miscellaneous map lemmas

Compare with previous version

I hope I resolved those conflicts properly... should be ready again.

resolved all threads

added 1 commit

• 32b96688 - miscellaneous map lemmas

Compare with previous version

Modulo minor comments, this seems OK.

added 1 commit

• d24fe4ce - nonzero → ne_0

Compare with previous version

resolved all threads

added 1 commit

• e05b6af1 - map_size_eq → map_to_list_length

Compare with previous version

resolved all threads