Add some list lemmas

This fixes some inconsistencies and gaps that I noticed while working on !439, and ports some list lemmas from Perennial.

mentioned in merge request !439

added 1 commit

• ef734bd6 - more list subseteq lemmas (some of them from Perennial)

Compare with previous version

mentioned in merge request !455 (merged)

Various comments.

added 1 commit

• 04e3ae30 - simplifications and formatting

Compare with previous version

resolved all threads

added 56 commits

• 04e3ae30...0727c134 - 51 commits from branch master
• 4558208d - list: add some missing lemmas, and small fixes
• 7b6f66a5 - port some list lemmas from Perennial
• 1c8dddc5 - more list subseteq lemmas (some of them from Perennial)
• 6e6d33c7 - simplifications and formatting
• 909b0681 - make head_replicate_Some a biimplication; list_prefix_eq moved to another MR

Compare with previous version

All comments resolved, ready for review again.

added 2 commits

• 7a10ad67 - simplifications and formatting
• 00a8fb07 - make head_replicate_Some a biimplication; list_prefix_eq moved to another MR

Compare with previous version

added 1 commit

• 2121847d - naming

Compare with previous version

resolved all threads