Add some list lemmas

Merged Ralf Jung requested to merge ralf/list into master

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

Merge request reports