diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36f0f1301c92a2414317d374cd52944d5c726367..b5ec4788938b54b36974be8ef11e3bca56d891a4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,6 +29,7 @@ API-breaking change is listed.
 - Add tactic `learn_hyp` (by Michael Sammler).
 - Add `Countable` instance for decidable Sigma types (by Simon Gregersen).
 - Add tactics `compute_done` and `compute_by` for solving goals by computation.
+- Add `Inj` instances for `fmap` on option and maps.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 1f0bc31b3cbb19b6ec5531dba436d5423598d24c..45a0cc67c8a0ec769052f38eb5f7f1a83cfda162 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -663,6 +663,13 @@ Lemma delete_singleton_ne {A} i j (x : A) :
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
 (** ** Properties of the map operations *)
+Global Instance map_fmap_inj {A B} (f : A → B) :
+  Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
+Proof.
+  intros ? m1 m2 Hm. apply map_eq; intros i.
+  apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
+Qed.
+
 Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
   (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
 Proof. rewrite lookup_fmap, fmap_Some. naive_solver. Qed.
diff --git a/theories/option.v b/theories/option.v
index 8ca6196886f812c19750db73bf99e0e03a92e0eb..576edfccc16bba1d480dd77c5dc9ca570502467c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -175,6 +175,10 @@ Global Instance option_fmap: FMap option := @option_map.
 Global Instance option_guard: MGuard option := λ P dec A f,
   match dec with left H => f H | _ => None end.
 
+Global Instance option_fmap_inj {A B} (f : A → B) :
+  Inj (=) (=) f → Inj (=@{option A}) (=@{option B}) (fmap f).
+Proof. intros ? [x1|] [x2|] [=]; naive_solver. Qed.
+
 Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
 Proof. unfold is_Some; destruct mx; naive_solver. Qed.
 Lemma fmap_Some {A B} (f : A → B) mx y :
@@ -210,6 +214,7 @@ Proof. intros; destruct mx; f_equal/=; auto. Qed.
 Lemma option_fmap_equiv_ext {A} `{Equiv B} (f g : A → B) (mx : option A) :
   (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
 Proof. destruct mx; constructor; auto. Qed.
+
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
   (f <$> mx) ≫= g = mx ≫= g ∘ f.
 Proof. by destruct mx. Qed.