Skip to content

More proper/non-expansiveness results for maps, lists, and big ops

Robbert Krebbers requested to merge robbert/big_op_proper into master

Creating an MR since I changed some internal lemmas, so we can track these changes if other developments make use of these internals.

Merge request reports