diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 159a09b5ae02e28cbbfdc268f2704109535a512a..a889f5924601ba44acc84646d1fcf1cf723a7f04 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -84,6 +84,11 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
+(** Copies of some definitions so we can control their unfolding *)
 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 _ _ _ !_ /.
+Arguments option_bind {_ _} _ !_ / : assert.
+
+Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
+  match mx with None => y | Some x => f x end.
+Arguments from_option {_ _} _ _ !_ / : assert.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index c473a31007e6e350d85e9ed99cc8f1321a586df9..76ba02c85451031d57c34f09b989a11a986b75ef 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -851,7 +851,7 @@ Proof.
   rewrite /ElimAcc /IntoAcc /ElimInv.
   iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
   iApply (Helim with "[Hcont]").
-  - iIntros (x) "Hα". iApply "Hcont". iSplitL; done.
+  - iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
   - iApply (Hacc with "Hinv Hin"). done.
 Qed.
 
@@ -860,7 +860,7 @@ Global Instance elim_inv_acc_with_close {X : Type}
        M1 M2 α β γ Q Q' :
   IntoAcc Pinv φ Pin M1 M2 α β γ →
   (∀ R, ElimModal True false false (M1 R) R Q Q') →
-  ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x -∗ M2 (default emp (γ x) id)))%I
+  ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x -∗ M2 (proofmode.base.from_option id emp (γ x))))%I
           Q (λ _, Q').
 Proof.
   rewrite /ElimAcc /IntoAcc /ElimInv.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 0801c091b666c63a83aa01c4d679ab614202d16d..bb6dfb416866c232ecaaa8f9ae6b27a39de3f4ec 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1101,7 +1101,7 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
   φ →
   (∀ R, ∃ Δ'',
     envs_app false (Esnoc Enil j
-                    (Pin -∗ (∀ x, Pout x -∗ default (Q' x) Pclose (λ Pclose, Pclose x -∗ Q' x)) -∗ R)%I) Δ'
+            (Pin -∗ (∀ x, Pout x -∗ from_option (λ Pclose, Pclose x -∗ Q' x) (Q' x) Pclose) -∗ R)%I) Δ'
       = Some Δ'' ∧
     envs_entails Δ'' R) →
   envs_entails Δ Q.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 613a1386a9d526fa171e9b94fac7fd69c4f687f4..920fa28677f11f26d2d960bffd40dfcf384df782 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -7,8 +7,11 @@ From stdpp Require Import hlist pretty.
 Set Default Proof Using "Type".
 Export ident.
 
+(** These are all proofmode-internal definitions and hence unfolding them should
+not affect the user's goal. *)
+(* TODO: Can we option_bind, from_option, maybe_wand reduce only if applied to a constructor? *)
 Declare Reduction env_cbv := cbv [
-  option_bind from_option (* TODO: Can we make these (and maybe_wand) reduce only if applied to a constructor? *)
+  option_bind from_option
   beq ascii_beq string_beq positive_beq Pos.succ ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom