diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index af8e2ab967e5945d2b7f9086fbe5b79db75320e8..8b61b8196a0337f7a8baf3f362e736502a7b3b62 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -87,13 +87,13 @@ Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 (** Soundness statement: facts derived in the logic / under modalities also hold
 outside the logic / without the modalities.
 (The other modalities, â–¡ and â– , can simply be stripped so they are obvious.) *)
-Lemma bupd_plain_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
+Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
 Proof. rewrite bupd_plain. done. Qed.
 
 Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
 Proof. induction n; eauto using later_soundness. Qed.
 
-Lemma modal_plain_soundness P `{!Plain P} n :
+Lemma modal_soundness P `{!Plain P} n :
   (⊢ Nat.iter n (bupd ∘ bi_later) P) → ⊢ P.
 Proof.
   intros H. apply (laterN_soundness _ n).
@@ -115,7 +115,7 @@ Proof. intros H. by eapply pure_soundness. Qed.
 Corollary consistency_modal n :
   ¬ ⊢@{uPredI M} Nat.iter n (bupd ∘ bi_later) False.
 Proof.
-  intros H. eapply pure_soundness, modal_plain_soundness, H.
+  intros H. eapply pure_soundness, modal_soundness, H.
   apply _.
 Qed.
 
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 9e5b9737fe7ae38b815387044d4f343cd659a2b3..582e0111c748994e5a8fd703eeddd833fe6993fb 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -135,7 +135,7 @@ Qed.
 (** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
   these cannot be used for anything. They are merely provided to enable making
   the adequacy proof generic in whether later credits are used. *)
-Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
+Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
@@ -148,10 +148,10 @@ Proof.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma fupd_plain_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
+Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
   (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ⊢@{iPropI Σ} |={E1,E2}=> P) → ⊢ P.
 Proof.
-  iIntros (Hfupd). eapply (lc_plain_soundness (S n)); first done.
+  iIntros (Hfupd). eapply (lc_soundness (S n)); first done.
   intros Hc. rewrite lc_succ.
   iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
   iMod wsat_alloc as (Hw) "[Hw HE]".
@@ -167,26 +167,26 @@ Qed.
 
 (** Generic soundness lemma for the fancy update, parameterized by [use_credits]
   on whether to use credits or not. *)
-Lemma fupd_plain_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
+Lemma fupd_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
   (hlc : has_lc) n E1 E2 :
   (∀ `{Hinv : invGS_gen hlc Σ},
     £ n ={E1,E2}=∗ P) →
   ⊢ P.
 Proof.
   destruct hlc.
-  - apply fupd_plain_soundness_lc. done.
-  - apply fupd_plain_soundness_no_lc. done.
+  - apply fupd_soundness_lc. done.
+  - apply fupd_soundness_no_lc. done.
 Qed.
 
 (** [step_fupdN] soundness lemmas *)
 
-Lemma step_fupdN_plain_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
   apply (laterN_soundness _  (S n)); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ m)=> Hinv. iIntros "Hc".
+  apply (fupd_soundness_no_lc ⊤ ⊤ _ m)=> Hinv. iIntros "Hc".
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   iApply fupd_plainly_mask_empty. iSpecialize ("H" with "Hc").
   iMod (step_fupdN_plain with "H") as "H". iMod "H". iModIntro.
@@ -194,11 +194,11 @@ Proof.
   iNext. iMod "H" as "#H". auto.
 Qed.
 
-Lemma step_fupdN_plain_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n P) →
   ⊢ P.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_plain_soundness_no_lc _ n m)=>Hinv.
+  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
   iIntros "Hcred". destruct n as [|n].
   { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
    simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
@@ -206,12 +206,12 @@ Proof.
   simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
 Qed.
 
-Lemma step_fupdN_plain_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
-  eapply (fupd_plain_soundness_lc (m + n)); [apply _..|].
+  eapply (fupd_soundness_lc (m + n)); [apply _..|].
   iIntros (Hinv) "Hlc". rewrite lc_split.
   iDestruct "Hlc" as "[Hm Hn]". iMod (Hiter with "Hm") as "Hupd".
   clear Hiter.
@@ -222,16 +222,16 @@ Proof.
     by iApply ("IH" with "Hn Hupd").
 Qed.
 
-Lemma step_fupdN_plain_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
+Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
   (∀ `{Hinv: !invGS_gen hlc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
-  eapply (fupd_plain_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
+  eapply (fupd_soundness_lc (m + n) ⊤ ⊤); [apply _..|].
   iIntros (Hinv) "Hlc". rewrite lc_split.
   iDestruct "Hlc" as "[Hm Hn]". iPoseProof (Hiter with "Hm") as "Hupd".
   clear Hiter.
-  (* FIXME can we reuse [step_fupdN_plain_soundness_lc] instead of redoing the induction? *)
+  (* FIXME can we reuse [step_fupdN_soundness_lc] instead of redoing the induction? *)
   iInduction n as [|n] "IH"; simpl.
   - by iModIntro.
   - rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
@@ -241,13 +241,13 @@ Qed.
 
 (** Generic soundness lemma for the fancy update, parameterized by [use_credits]
   on whether to use credits or not. *)
-Lemma step_fupdN_plain_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
+Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
   (hlc : has_lc) (n m : nat) :
   (∀ `{Hinv : invGS_gen hlc Σ},
     £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   destruct hlc.
-  - apply step_fupdN_plain_soundness_lc. done.
-  - apply step_fupdN_plain_soundness_no_lc. done.
+  - apply step_fupdN_soundness_lc. done.
+  - apply step_fupdN_soundness_no_lc. done.
 Qed.
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index b787593a7ed4fd42c0bee8a6a0294e3ccf557c90..09b55d1c71ac84799ea45881aa2f3b5830ccb4ad 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -357,11 +357,11 @@ Module le_upd.
     iModIntro. iExists C. iFrame.
   Qed.
 
-  Lemma lc_plain_soundness `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
+  Lemma lc_soundness `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
     (∀ {Hc: lcGS Σ}, £ m -∗ |==£> P) → ⊢ P.
   Proof.
     intros H. apply (laterN_soundness _ (S m)).
-    eapply bupd_plain_soundness; first apply _.
+    eapply bupd_soundness; first apply _.
     iStartProof.
     iMod (lc_alloc m) as (C) "[H● H◯]".
     iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "Hâ—¯").
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ccd97d2d190eac2f24b3e50e59c3d38675e09c4b..af16bb748bd4b77a9cd8de81851118dd95fb81a2 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -156,7 +156,7 @@ Local Lemma wp_progress_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} es σ1 n κs t2
 Proof.
   iIntros (Hwp ??).
   eapply pure_soundness.
-  eapply (step_fupdN_plain_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
+  eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
   iIntros (Hinv) "Hcred".
   iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)".
@@ -214,7 +214,7 @@ Lemma wp_strong_adequacy_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s es σ1 n κs
 Proof.
   iIntros (Hwp ?).
   eapply pure_soundness.
-  eapply (step_fupdN_plain_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
+  eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
   iIntros (Hinv) "Hcred".
   iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 6e295a13067ebd50d6dbbfdea57f4fda0e49d881..64e52d0fa80eb36ba3300850415a5626931719a1 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -134,7 +134,7 @@ Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv. iIntros "_".
+  apply (fupd_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv. iIntros "_".
   iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
   set (iG := IrisG Hinv stateI fork_post num_laters_per_step stateI_mono).
   iApply (@twptp_total _ _ iG _ n with "Hσ").