stdlib: fixed lemma map.Occ.occ_exchange

f2a36c56 · Jean-Christophe Filliâtre · 53bba4a2 · f2a36c56
Commit f2a36c56 authored Jan 18, 2018 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

stdlib/map.mlw stdlib/map.mlw +1 -1

No files found.
--- a/stdlib/map.mlw
+++ b/stdlib/map.mlw
@@ -160,7 +160,7 @@ module Occ

  lemma occ_exchange :
    forall m: map int 'a, l u i j: int, x y z: 'a.
-    l <= i < u -> l <= j < u ->
+    l <= i < j < u ->
    occ z m[i <- x][j <- y] l u =
    occ z m[i <- y][j <- x] l u