More consistent naming for CMRA/uPred duplication lemmas.

algebra/cmra.v

@@ -320,10 +320,10 @@ Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
 Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed. 
 Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
 Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed. 
-Lemma cmra_pcore_pcore x cx : pcore x = Some cx → cx ⋅ cx ≡ cx.
-Proof. eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
-Lemma cmra_pcore_pcore' x cx : pcore x ≡ Some cx → cx ⋅ cx ≡ cx.
-Proof. eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
+Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
+Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
+Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
+Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
 Lemma cmra_pcore_validN n x cx : ✓{n} x → pcore x = Some cx → ✓{n} cx.
 Proof.
   intros Hvx Hx%cmra_pcore_l. move: Hvx; rewrite -Hx. apply cmra_validN_op_l.
@@ -333,6 +333,10 @@ Proof.
   intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
 Qed.
 
+(** ** Persistent elements *)
+Lemma persistent_dup x `{!Persistent x} : x ≡ x ⋅ x.
+Proof. by apply cmra_pcore_dup' with x. Qed.
+
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
 Proof. intros [z ->]. by exists z. Qed.
@@ -428,8 +432,8 @@ Section total_core.
 
   Lemma cmra_core_r x : x ⋅ core x ≡ x.
   Proof. by rewrite (comm _ x) cmra_core_l. Qed.
-  Lemma cmra_core_core x : core x ⋅ core x ≡ core x.
-  Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
+  Lemma cmra_core_dup x : core x ≡ core x ⋅ core x.
+  Proof. by rewrite -{3}(cmra_core_idemp x) cmra_core_r. Qed.
   Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
   Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
   Lemma cmra_core_valid x : ✓ x → ✓ core x.

algebra/upred.v

@@ -876,7 +876,7 @@ 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_core; auto.
+  exists (core x), (core x); rewrite -cmra_core_dup; auto.
 Qed.
 Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊢ (□ P ★ Q).
 Proof.