Remove primitive rule `□ (P ∧ Q) ⊢ □ (P ∗ Q)`.

It can be derived, thanks to Ales for noticing!

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.

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 *.