diff --git a/prelude/option.v b/prelude/option.v
index 0ceac790cc6bc3b1284120550c52d6c494a07eab..dfaf08a43e647d7e7ce6140f062c512438661122 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -118,6 +118,8 @@ Section setoids.
   Proof. apply _. Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
   Proof. by constructor. Qed.
+  Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A).
+  Proof. by inversion_clear 1. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
   Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.