diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 4ff779335013ce517652eda6467683823c1948ec..9497be34506b4e7f20a132cc2a9f892aeefffdbb 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -83,3 +83,7 @@ Qed.
 
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
+
+Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
+  match mx with Some x => f x | None => None end.
+Arguments option_bind _ _ _ !_ /.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index dafac376dec5d49b64b5df41781e0c0d3d0a3de4..a6729546dd29b3baf450cc0664a13ae4d7bda5b3 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -361,7 +361,7 @@ Proof.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
-  destruct d; simplify_eq; solve_sep_entails.
+  destruct d; simplify_eq/=; solve_sep_entails.
 Qed.
 
 Global Instance envs_Forall2_refl (R : relation (uPred M)) :
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index c3136b8b86eacc4408e0d116d8f6f35dcbd73914..d980e776fed0384f999a229883869dceb507f82d 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -17,8 +17,8 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   end.
 
 Module env_notations.
-  Notation "y ≫= f" := (match y with Some x => f x | None => None end).
-  Notation "x ← y ; z" := (match y with Some x => z | None => None end).
+  Notation "y ≫= f" := (option_bind f y).
+  Notation "x ← y ; z" := (y ≫= λ x, z).
   Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
   Notation "Γ !! j" := (env_lookup j Γ).
 End env_notations.
@@ -93,6 +93,8 @@ Ltac simplify :=
   | _ => progress simplify_eq/=
   | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
   | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
+  | H : context [option_bind _ ?x] |- _ => destruct x eqn:?
+  | |- context [option_bind _ ?x] => destruct x eqn:?
   | _ => case_match
   end.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 94c2de629d210d0464db5f293d82d0ce1baf62e6..36b2006c69cf4e84e586c22de6f0ae4b7bcf3f90 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -8,6 +8,7 @@ Set Default Proof Using "Type".
 Export ident.
 
 Declare Reduction env_cbv := cbv [
+  option_bind
   beq ascii_beq string_beq positive_beq ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_persistent env_spatial env_spatial_is_nil envs_dom