diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 904a1eef213342435cfcc9eaff28b9c7da50b66d..cc6f3af304e0fef9599735b62022d3f93e31ab4e 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -479,6 +479,8 @@ Proof. intros P Q; apply always_mono. Qed.
 
 Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros <-. apply always_idemp. Qed.
+Lemma always_idemp P : □ □ P ⊣⊢ □ P.
+Proof. apply (anti_symm _); auto using always_idemp. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. apply (anti_symm _); auto using always_pure_2. Qed.
@@ -509,16 +511,20 @@ Proof.
   rewrite -(internal_eq_refl a) always_pure; auto.
 Qed.
 
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed.
 Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
 Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
 Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
+Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
+Proof. by rewrite -always_and_sep_l' idemp. Qed.
+
+Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Proof.
+  apply (anti_symm (⊢)); auto.
+  rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
+Qed.
 Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
-Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
 
 Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
 Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 12a444c5921b47880c2f26a867fe3a7cf251c2f0..16d109fe87360e70ca8366e535e5c629f499cfa3 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -437,11 +437,6 @@ Proof. by unseal. Qed.
 Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
 Proof. by unseal. Qed.
 
-Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q).
-Proof.
-  unseal; split=> n x ? [??].
-  exists (core x), (core x); rewrite -cmra_core_dup; auto.
-Qed.
 Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   unseal; split=> n x ? [??]; exists (core x), x; simpl in *.