diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index cc6f3af304e0fef9599735b62022d3f93e31ab4e..629d54ccf1a868be7d7516dce68b536e696217ed 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -478,9 +478,9 @@ Global Instance always_flip_mono' :
 Proof. intros P Q; apply always_mono. Qed.
 
 Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros <-. apply always_idemp. Qed.
+Proof. intros <-. apply always_idemp_2. Qed.
 Lemma always_idemp P : □ □ P ⊣⊢ □ P.
-Proof. apply (anti_symm _); auto using always_idemp. Qed.
+Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. apply (anti_symm _); auto using always_pure_2. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 16d109fe87360e70ca8366e535e5c629f499cfa3..0b84b8d5974fe2ee172c5f76c9e35680a95a6a60 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -427,7 +427,7 @@ Proof.
   unseal; split=> n x ? /=.
   eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
 Qed.
-Lemma always_idemp P : □ P ⊢ □ □ P.
+Lemma always_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
 Lemma always_pure_2 φ : ⌜φ⌝ ⊢ □ ⌜φ⌝.