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