More proper/non-expansiveness results for maps, lists, and big ops
Creating an MR since I changed some internal lemmas, so we can track these changes if other developments make use of these internals.
Creating an MR since I changed some internal lemmas, so we can track these changes if other developments make use of these internals.