Let always_idemp be the rule `□ □ P ⊣⊢ □ P` in both ways.

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.

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 φ : ⌜φ⌝ ⊢ □ ⌜φ⌝.