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.