Commit c6e8c5d5 authored by Robbert Krebbers's avatar Robbert Krebbers

More permissive `gmap_fmap_mono`.

parent 19aae59a
...@@ -475,7 +475,7 @@ Proof. ...@@ -475,7 +475,7 @@ Proof.
[done|by rewrite lookup_singleton]. [done|by rewrite lookup_singleton].
Qed. Qed.
Lemma gmap_fmap_mono {B : ucmraT} (f : A B) m1 m2 : Lemma gmap_fmap_mono {B : cmraT} (f : A B) m1 m2 :
Proper (() ==> ()) f Proper (() ==> ()) f
( x y, x y f x f y) m1 m2 fmap f m1 fmap f m2. ( x y, x y f x f y) m1 m2 fmap f m1 fmap f m2.
Proof. Proof.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment