diff --git a/theories/option.v b/theories/option.v
index cd88494a1fc46a18947289b54f97d308be8ddc1c..f2eed50fc86ad65a0e92354119a4fe1899398afc 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -225,6 +225,9 @@ Proof. intros. by apply option_bind_ext. Qed.
 Lemma bind_Some {A B} (f : A → option B) (mx : option A) y :
   mx ≫= f = Some y ↔ ∃ x, mx = Some x ∧ f x = Some y.
 Proof. destruct mx; naive_solver. Qed.
+Lemma bind_Some_equiv {A} `{Equiv B} (f : A → option B) (mx : option A) y :
+  mx ≫= f ≡ Some y ↔ ∃ x, mx = Some x ∧ f x ≡ Some y.
+Proof. destruct mx; (split; [inversion 1|]); naive_solver. Qed.
 Lemma bind_None {A B} (f : A → option B) (mx : option A) :
   mx ≫= f = None ↔ mx = None ∨ ∃ x, mx = Some x ∧ f x = None.
 Proof. destruct mx; naive_solver. Qed.