diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 53b19a8f73665b4b3dc65d1be536ffff5f41c43d..99c9f05b1bf7d9de27689f92af270a0f5e77bf1d 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.