diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 3b4142dc55f6438d22488255f3491b5c0dc6e626..0f2136dee15611aaa8d44300f51ea36d8a48fa72 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -57,9 +57,9 @@ Proof. solve_proper. Qed.
 Lemma ht_mono s E P P' Φ Φ' e :
   (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
-Lemma ht_stuckness_mono s1 s2 E P Φ e :
+Lemma ht_stuck_mono s1 s2 E P Φ e :
   (s1 ≤ s2)%stuckness → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
-Proof. by intros; apply persistently_mono, wand_mono, wp_stuckness_mono. Qed.
+Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed.
 Global Instance ht_mono' s E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
 Proof. solve_proper. Qed.
@@ -98,10 +98,10 @@ Proof.
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
 
-Lemma ht_forget_not_stuck s E P Φ e :
+Lemma ht_stuck_weaken s E P Φ e :
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
 Proof.
-  by iIntros "#Hwp !# ?"; iApply wp_forget_not_stuck; iApply "Hwp".
+  by iIntros "#Hwp !# ?"; iApply wp_stuck_weaken; iApply "Hwp".
 Qed.
 
 Lemma ht_mask_weaken s E1 E2 P Φ e :
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index a10f6027558550cca9eba4c2681f723efa7136ed..3fe7e6336f98e0b74d11d0ebab1b90ed97b73830 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -210,7 +210,7 @@ Proof.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
-Lemma wp_forget_not_stuck s E e Φ :
+Lemma wp_stuck_weaken s E e Φ :
   WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
@@ -311,9 +311,9 @@ Proof.
   iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto.
   iIntros "{$H}" (v) "?". by iApply HΦ.
 Qed.
-Lemma wp_stuckness_mono s1 s2 E e Φ :
+Lemma wp_stuck_mono s1 s2 E e Φ :
   (s1 ≤ s2)%stuckness → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
-Proof. case: s1; case: s2 => // _. exact: wp_forget_not_stuck. Qed.
+Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
 Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.
 Global Instance wp_mono' s E e :