diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d4dd56acc20d7634b4265659ea458162a41d2b08..c07f7aaa880160321e4d09ace1124c7af4533559 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.