From 7ef1770cb951927f3ddd58da0e3361498dd24add Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Jul 2022 23:21:26 +0200
Subject: [PATCH] Flip direction of `map_disjoint_fmap`.

---
 theories/fin_maps.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d4dd56ac..c07f7aaa 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2054,7 +2054,7 @@ Proof.
 Qed.
 
 Lemma map_disjoint_fmap {A B} (f1 f2 : A → B) (m1 m2 : M A) :
-  m1 ##ₘ m2 ↔ f1 <$> m1 ##ₘ f2 <$> m2.
+  f1 <$> m1 ##ₘ f2 <$> m2 ↔ m1 ##ₘ m2.
 Proof.
   rewrite !map_disjoint_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
 Qed.
-- 
GitLab