See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do
This rule expresses a form of "parametricity": it says that regardless of A, B, f, and b, the function map_fold f b m will always traverse the map m in the same order. Namely the order of converting the map into a list.
This law holds for all instances of FinMap we currently have, and I think without weird non-constructive axioms (that allow one to define non-parametric functions) it is impossible to define a FinMap instance that does not satisfy this law.
/cc @johannes @ivanbakel