diff --git a/CHANGELOG.md b/CHANGELOG.md
index 44a44bd475369f6417f2c4dc37dd28aa6266998d..10d4c4f02d99154a41ee86d2dfb16453ae62f5cd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,15 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   backwards incompatibility. This can usually be fixed by manually clearing some
   hypotheses. A more detailed description of the changes can be found in
   https://gitlab.mpi-sws.org/iris/iris/merge_requests/341.
+* Renamed some accessor-style lemmas to consistently use the suffix `_acc`
+  instead of `_open`:
+  `inv_open` -> `inv_acc`, `inv_open_strong` -> `inv_acc_strong`,
+  `inv_open_timeless` -> `inv_acc_timeless`, `na_inv_open` -> `na_inv_acc`,
+  `cinv_open` -> `cinv_acc`, `cinv_open_strong` -> `cinv_acc_strong`,
+  `auth_open` -> `auth_acc`, `sts_open` -> `sts_acc`.
+  To make this work we also had to rename `inv_acc` -> `inv_alter`.
+  (Most developments should be unaffected as the typical way to invoke these
+  lemmas is through `iInv`, and that does not change.)
 
 ## Iris 3.2.0 (released 2019-08-29)
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index d279aded7857a8d25a4a43db2b6509fcb0b6d3ee..5dad15580fb9025d8518a9e5a269191895c350ce 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -112,7 +112,7 @@ Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".
-  iMod (inv_open E N P with "Hinv") as "[HP Hclose]"=>//.
+  iMod (inv_acc E N P with "Hinv") as "[HP Hclose]"=>//.
   iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|].
   iIntros (v) "[HP $]". by iApply "Hclose".
 Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 0d754209f7303cc2554f0e785898e7b103cb839a..9e14b4cb338c065d1bbec646145e2306105d392c 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -132,7 +132,7 @@ Section auth.
   Lemma auth_empty γ : (|==> auth_own γ ε)%I.
   Proof. by rewrite /auth_own -own_unit. Qed.
 
-  Lemma auth_acc E γ a :
+  Lemma auth_inv_acc E γ a :
     ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t,
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
       ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E}=∗ ▷ auth_inv γ f φ ∗ auth_own γ b.
@@ -147,7 +147,7 @@ Section auth.
     iModIntro. iFrame. iExists u. iFrame.
   Qed.
 
-  Lemma auth_open E N γ a :
+  Lemma auth_acc E N γ a :
     ↑N ⊆ E →
     auth_ctx γ N f φ ∗ auth_own γ a ={E,E∖↑N}=∗ ∃ t,
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
@@ -155,15 +155,15 @@ Section auth.
   Proof using Type*.
     iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
-       [auth_acc] and [inv_open] -- but since we don't have any good support
+       [auth_inv_acc] and [inv_acc] -- but since we don't have any good support
        for that currently, this gets more tedious than it should, with us having
        to unpack and repack various proofs.
        TODO: Make this mostly automatic, by supporting "opening accessors
        around accessors". *)
-    iMod (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
+    iMod (auth_inv_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
     iModIntro. iExists t. iFrame. iIntros (u b) "H".
     iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
   Qed.
 End auth.
 
-Arguments auth_open {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
+Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 0aaa353d3e3b9448c95464273984574514748342..38f1a16b7dbdde8128baa289be8af6693684512d 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -109,13 +109,13 @@ Section proofs.
   Qed.
 
   (*** Accessors *)
-  Lemma cinv_open_strong E N γ p P :
+  Lemma cinv_acc_strong E N γ p P :
     ↑N ⊆ E →
     cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
     ▷ P ∗ cinv_own γ p ∗ (∀ E' : coPset, ▷ P ∨ cinv_own γ 1 ={E',↑N ∪ E'}=∗ True)).
   Proof.
     iIntros (?) "Hinv Hown".
-    iPoseProof (inv_open (↑ N) N with "Hinv") as "H"; first done.
+    iPoseProof (inv_acc (↑ N) N with "Hinv") as "H"; first done.
     rewrite difference_diag_L.
     iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
     rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
@@ -126,12 +126,12 @@ Section proofs.
     - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
   Qed.
 
-  Lemma cinv_open E N γ p P :
+  Lemma cinv_acc E N γ p P :
     ↑N ⊆ E →
     cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     iIntros (?) "#Hinv Hγ".
-    iMod (cinv_open_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
+    iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
     iIntros "!> HP".
     rewrite {2}(union_difference_L (↑N) E)=> //.
     iApply "H". by iLeft.
@@ -141,7 +141,7 @@ Section proofs.
   Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
   Proof.
     iIntros (?) "#Hinv Hγ".
-    iMod (cinv_open_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
+    iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
     rewrite {2}(union_difference_L (↑N) E)=> //.
     iApply "H". by iRight.
   Qed.
@@ -155,7 +155,7 @@ Section proofs.
   Proof.
     rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
     rewrite exist_unit -assoc.
-    iApply (cinv_open with "Hinv"); done.
+    iApply (cinv_acc with "Hinv"); done.
   Qed.
 End proofs.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index e14ca49393aa0fc8ce0771b26315d9f40604a70b..337e27bfdb96a0f74e5fc7e8db547fb9edefec82 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -27,7 +27,7 @@ Section inv.
   Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
     (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ ownI i P)%I.
 
-  Lemma own_inv_open E N P :
+  Lemma own_inv_acc E N P :
     ↑N ⊆ E → own_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
@@ -81,7 +81,7 @@ Section inv.
   Lemma own_inv_to_inv M P: own_inv M P  -∗ inv M P.
   Proof.
     iIntros "#I". rewrite inv_eq. iIntros (E H).
-    iPoseProof (own_inv_open with "I") as "H"; eauto.
+    iPoseProof (own_inv_acc with "I") as "H"; eauto.
   Qed.
 
   (** ** Public API of invariants *)
@@ -97,7 +97,7 @@ Section inv.
   Global Instance inv_persistent N P : Persistent (inv N P).
   Proof. rewrite inv_eq. apply _. Qed.
 
-  Lemma inv_acc N P Q:
+  Lemma inv_alter N P Q:
     inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
   Proof.
     rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
@@ -108,7 +108,7 @@ Section inv.
 
   Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q.
   Proof.
-    iIntros "#HPQ #HI". iApply (inv_acc with "HI").
+    iIntros "#HPQ #HI". iApply (inv_alter with "HI").
     iIntros "!> !# HP". iSplitL "HP".
     - by iApply "HPQ".
     - iIntros "HQ". by iApply "HPQ".
@@ -127,7 +127,7 @@ Section inv.
     iApply own_inv_to_inv. done.
   Qed.
 
-  Lemma inv_open E N P :
+  Lemma inv_acc E N P :
     ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
@@ -146,11 +146,11 @@ Section inv.
   Qed.
 
   (** ** Derived properties *)
-  Lemma inv_open_strong E N P :
+  Lemma inv_acc_strong E N P :
     ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True.
   Proof.
     iIntros (?) "Hinv".
-    iPoseProof (inv_open (↑ N) N with "Hinv") as "H"; first done.
+    iPoseProof (inv_acc (↑ N) N with "Hinv") as "H"; first done.
     rewrite difference_diag_L.
     iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
     rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
@@ -159,16 +159,16 @@ Section inv.
     by rewrite left_id_L.
   Qed.
 
-  Lemma inv_open_timeless E N P `{!Timeless P} :
+  Lemma inv_acc_timeless E N P `{!Timeless P} :
     ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
   Proof.
-    iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
+    iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
   Lemma inv_sep_l N P Q : inv N (P ∗ Q) -∗ inv N P.
   Proof.
-    iIntros "#HI". iApply inv_acc; eauto.
+    iIntros "#HI". iApply inv_alter; eauto.
     iIntros "!> !# [$ $] $".
   Qed.
 
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index eff3c4abc521d9c22be852ddd5df3ff373b23097..40b9d06712268ede97b35eb8deeec4e7dbffafed 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -91,7 +91,7 @@ Section proofs.
     iNext. iLeft. by iFrame.
   Qed.
 
-  Lemma na_inv_open p E F N P :
+  Lemma na_inv_acc p E F N P :
     ↑N ⊆ E → ↑N ⊆ F →
     na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
                        (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
@@ -121,6 +121,6 @@ Section proofs.
   Proof.
     rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
     rewrite exist_unit -assoc /=.
-    iApply (na_inv_open with "Hinv"); done.
+    iApply (na_inv_acc with "Hinv"); done.
   Qed.
 End proofs.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index ad55707f2192ada2f8fb50538395cd417562a537..6b6b748e4fc9209dc5a876b21e619fccb65ca35d 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -126,7 +126,7 @@ Section sts.
     rewrite /sts_inv. iNext. iExists s. by iFrame.
   Qed.
 
-  Lemma sts_accS φ E γ S T :
+  Lemma sts_inv_accS φ E γ S T :
     ▷ sts_inv γ φ ∗ sts_ownS γ S T ={E}=∗ ∃ s,
       ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
@@ -144,13 +144,13 @@ Section sts.
     iModIntro. iNext. iExists s'; by iFrame.
   Qed.
 
-  Lemma sts_acc φ E γ s0 T :
+  Lemma sts_inv_acc φ E γ s0 T :
     ▷ sts_inv γ φ ∗ sts_own γ s0 T ={E}=∗ ∃ s,
       ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
-  Proof. by apply sts_accS. Qed.
+  Proof. by apply sts_inv_accS. Qed.
 
-  Lemma sts_openS φ E N γ S T :
+  Lemma sts_accS φ E N γ S T :
     ↑N ⊆ E →
     sts_ctx γ N φ ∗ sts_ownS γ S T ={E,E∖↑N}=∗ ∃ s,
       ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
@@ -158,22 +158,22 @@ Section sts.
   Proof.
     iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
-       [sts_acc] and [inv_open] -- but since we don't have any good support
+       [sts_inv_acc] and [inv_acc] -- but since we don't have any good support
        for that currently, this gets more tedious than it should, with us having
        to unpack and repack various proofs.
        TODO: Make this mostly automatic, by supporting "opening accessors
        around accessors". *)
-    iMod (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
+    iMod (sts_inv_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
     iModIntro. iExists s. iFrame. iIntros (s' T') "H".
     iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
   Qed.
 
-  Lemma sts_open φ E N γ s0 T :
+  Lemma sts_acc φ E N γ s0 T :
     ↑N ⊆ E →
     sts_ctx γ N φ ∗ sts_own γ s0 T ={E,E∖↑N}=∗ ∃ s,
       ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
-  Proof. by apply sts_openS. Qed.
+  Proof. by apply sts_accS. Qed.
 End sts.
 
 Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 646cd12abbd7ddcdbcbc7c5f1c134242db7fb472..594799bf0ca9717c298aa20b722f412a5729b7c1 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -87,7 +87,7 @@ Module inv. Section inv.
   Arguments inv _ _%I.
   Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
   Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
-  Hypothesis inv_open :
+  Hypothesis inv_fupd :
     ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).
 
   (* We have tokens for a little "two-state STS": [start] -> [finish].
@@ -113,9 +113,9 @@ Module inv. Section inv.
   Hypothesis consistency : ¬ (fupd M1 False).
 
   (** Some general lemmas and proof mode compatibility. *)
-  Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
+  Lemma inv_fupd' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
   Proof.
-    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
+    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_fupd; last first.
     { iSplit; first done. iExact "HP". }
     iIntros "(HP & HPw)". by iApply "HPw".
   Qed.
@@ -167,7 +167,7 @@ Module inv. Section inv.
   Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q).
   Proof.
     iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
-    iApply (inv_open' i). iSplit; first done.
+    iApply (inv_fupd' i). iSplit; first done.
     iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
     { iDestruct "HaP" as "[Hs | [Hf _]]".
       - by iApply start_finish.
@@ -176,7 +176,7 @@ Module inv. Section inv.
     iApply fupd_intro. iSplitL "Hf'"; first by eauto.
     (* Step 2: Open the Q-invariant. *)
     iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
-    iApply (inv_open' i). iSplit; first done.
+    iApply (inv_fupd' i). iSplit; first done.
     iIntros "[HaQ | [_ #HQ]]".
     { iExFalso. iApply finished_not_start. by iFrame. }
     iApply fupd_intro. iSplitL "Hf".
@@ -308,7 +308,7 @@ Module linear2. Section linear2.
   Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP).
   Hypothesis cinv_alloc : ∀ E,
     fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ))%I.
-  Hypothesis cinv_access : ∀ P γ,
+  Hypothesis cinv_acc : ∀ P γ,
     cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
 
   (** Some general lemmas and proof mode compatibility. *)
@@ -335,7 +335,7 @@ Module linear2. Section linear2.
     iIntros "HP".
     iMod cinv_alloc as (γ) "Hmkinv".
     iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
-    iMod (cinv_access with "Hinv Htok") as "(Htrue & Htok & Hclose)".
+    iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
     iApply "Hclose". done.
   Qed.
 End linear2. End linear2.