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