diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 05272e82ae1d5570d1a38950c85297ec0f440790..5f5e702be1364229750ed80d1584cf609b555a0b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -174,6 +174,11 @@ Section setoid.
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
+  Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).
+  Proof.
+    intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
+  Qed.
 End setoid.
 
 (** ** General properties *)
diff --git a/theories/option.v b/theories/option.v
index 24552ced1403e78b31bb46282e3c0d65795d2274..5af4b5a039438871f4996114956b1acd1153b071 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -207,6 +207,10 @@ Proof. destruct mx; naive_solver. Qed.
 Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
 Proof. by destruct mx. Qed.
 
+Instance option_fmap_proper `{Equiv A, Equiv B} (f : A → B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=option) f).
+Proof. destruct 2; constructor; auto. Qed.
+
 (** ** Inverses of constructors *)
 (** We can do this in a fancy way using dependent types, but rewrite does
 not particularly like type level reductions. *)