diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 82d6cf0796e48cb9a3905e986cd4a5ba5dc1bd5c..bf8dc1550ae7d462be94bd4d01ffb3a1a875fa1e 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1330,6 +1330,10 @@ Proof.
     apply optionO_map_ne, oFunctor_map_contractive.
 Qed.
 
+Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
+Proof. apply option_fmap_inj. Qed.
+
 (** * Later type *)
 (** Note that the projection [later_car] is not non-expansive (see also the
 lemma [later_car_anti_contractive] below), so it cannot be used in the logic.