occ_exchange
Hello,
I was looking at the current status of the Coq realizations in master. I don't know very well these theories but I found this lemma in map.mlw which I think may be wrong when x <> y && x = z && i = j
:
lemma occ_exchange :
forall m: map int 'a, l u i j: int, x y z: 'a.
l <= i < u -> l <= j < u ->
occ z m[i <- x][j <- y] l u =
occ z m[i <- y][j <- x] l u