diff --git a/algebra/cmra.v b/algebra/cmra.v
index fe76e9cbb9a91bf7f1750da556fb924eab21d579..5c8a685e9ea235e38ed8a3a2d3b6f3d85c6c7c2e 100644
--- a/algebra/cmra.v
+++ b/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.
diff --git a/algebra/upred.v b/algebra/upred.v
index 0a72da7b07a5f0c63b8aebaa0117409a61a7bd42..a354f58b1b3f9d828cc2f1c6c2d017ca8adc274a 100644
--- a/algebra/upred.v
+++ b/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.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index f76f90338ba71d8ee20768b2e8d1d9acee11b853..013de3e6b1c0e3d71956e857f41d8725f266acdb 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -112,7 +112,7 @@ Section gmap.
   Implicit Types Φ Ψ : K → A → uPred M.
 
   Lemma big_sepM_mono Φ Ψ m1 m2 :
-    m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
+    m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
   Proof.
     intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
@@ -121,7 +121,7 @@ Section gmap.
       apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
   Qed.
   Lemma big_sepM_proper Φ Ψ m1 m2 :
-    m1 ≡ m2 → (∀ x k, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
+    m1 ≡ m2 → (∀ k x, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m1, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
   Proof.
     (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
@@ -149,14 +149,30 @@ Section gmap.
 
   Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
   Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
+
   Lemma big_sepM_insert Φ (m : gmap K A) i x :
     m !! i = None →
     ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ m, Φ k y).
   Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
+  Lemma big_sepM_fn_insert (Ψ : K → A → uPred M → uPred M) (Φ : K → uPred M) m i x P :
+    m !! i = None →
+       ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=P]> Φ k))
+    ⊣⊢ (Ψ i x P ★ [★ map] k↦y ∈ m, Ψ k y (Φ k)).
+  Proof.
+    intros. rewrite big_sepM_insert // fn_lookup_insert.
+    apply sep_proper, big_sepM_proper; auto=> k y ??.
+    by rewrite fn_lookup_insert_ne; last set_solver.
+  Qed.
+  Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
+    m !! i = None →
+    ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
+  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
+
   Lemma big_sepM_delete Φ (m : gmap K A) i x :
     m !! i = Some x →
     ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y).
   Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed.
+
   Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
   Proof.
     rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
@@ -222,7 +238,7 @@ Section gset.
   Lemma big_sepS_insert Φ X x :
     x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y).
   Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
-  Lemma big_sepS_insert' (Ψ : A → uPred M → uPred M) Φ X x P :
+  Lemma big_sepS_fn_insert (Ψ : A → uPred M → uPred M) Φ X x P :
     x ∉ X →
        ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=P]> Φ y))
     ⊣⊢ (Ψ x P ★ [★ set] y ∈ X, Ψ y (Φ y)).
@@ -231,9 +247,9 @@ Section gset.
     apply sep_proper, big_sepS_proper; auto=> y ??.
     by rewrite fn_lookup_insert_ne; last set_solver.
   Qed.
-  Lemma big_sepS_insert'' Φ X x P :
+  Lemma big_sepS_fn_insert' Φ X x P :
     x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
-  Proof. apply (big_sepS_insert' (λ y, id)). Qed.
+  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
 
   Lemma big_sepS_delete Φ X x :
     x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y).
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 99a9f6ed0c522497923afe636fb922e87bb30ad0..feeeabfe57be0520719c0940a82bf995eacf407d 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -88,9 +88,9 @@ Proof.
     iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
     iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
     iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
-    rewrite -assoc_L !big_sepS_insert''; [|abstract set_solver ..].
+    rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
     by iFrame "HR1 HR2".
-  - rewrite -assoc_L !big_sepS_insert'; [|abstract set_solver ..].
+  - rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..].
     by repeat iSplit.
 Qed.
 
diff --git a/prelude/base.v b/prelude/base.v
index ff635a1a3cf0bc5b84a3fc2ba9aff9572e0f34cd..22752705fcfc727038368eb0053fb2d86e83e8c3 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -316,7 +316,6 @@ Arguments compose _ _ _ _ _ _ /.
 Arguments flip _ _ _ _ _ _ /.
 Arguments const _ _ _ _ /.
 Typeclasses Transparent id compose flip const.
-Instance: Params (@pair) 2.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
@@ -402,6 +401,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
 Notation "p .1" := (fst p) (at level 10, format "p .1").
 Notation "p .2" := (snd p) (at level 10, format "p .2").
 
+Instance: Params (@pair) 2.
+
 Notation curry := prod_curry.
 Notation uncurry := prod_uncurry.
 Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 7a308038c82b3749d6661bf16cea7ac0e060df21..72737d70d8fcb413d79a116d7e01f6f6a29a2952 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -717,14 +717,34 @@ Qed.
 Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
   sep_destruct : □?p P ⊢ □?p (Q1 ★ Q2).
 Arguments sep_destruct : clear implicits.
+Class OpDestruct {A : cmraT} (a b1 b2 : A) :=
+  op_destruct : a ≡ b1 ⋅ b2.
+Arguments op_destruct {_} _ _ _ {_}.
+
+Global Instance op_destruct_op {A : cmraT} (a b : A) : OpDestruct (a â‹… b) a b.
+Proof. by rewrite /OpDestruct. Qed.
+Global Instance op_destruct_persistent {A : cmraT} (a : A) :
+  Persistent a → OpDestruct a a a.
+Proof. intros; apply (persistent_dup a). Qed.
+Global Instance op_destruct_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  OpDestruct a b1 b2 → OpDestruct a' b1' b2' →
+  OpDestruct (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
+  OpDestruct a b1 b2 → OpDestruct (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+
 Lemma sep_destruct_spatial p P Q1 Q2 : P ⊢ (Q1 ★ Q2) → SepDestruct p P Q1 Q2.
 Proof. rewrite /SepDestruct=> ->. by rewrite always_if_sep. Qed.
 
 Global Instance sep_destruct_sep p P Q : SepDestruct p (P ★ Q) P Q.
-Proof. by apply sep_destruct_spatial. Qed.
-Global Instance sep_destruct_ownM p (a b : M) :
-  SepDestruct p (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b).
-Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.
+Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
+Global Instance sep_destruct_ownM p (a b1 b2 : M) :
+  OpDestruct a b1 b2 →
+  SepDestruct p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  rewrite /OpDestruct /SepDestruct=> ->. by rewrite ownM_op always_if_sep.
+Qed.
 
 Global Instance sep_destruct_and P Q : SepDestruct true (P ∧ Q) P Q.
 Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
index 496b63049a51471eb990d07d3cdb43c2f034767a..87b8e0ef366fca8ff4a7e7addd186fc601bd451f 100644
--- a/proofmode/ghost_ownership.v
+++ b/proofmode/ghost_ownership.v
@@ -6,9 +6,9 @@ Section ghost.
 Context `{inG Λ Σ A}.
 Implicit Types a b : A.
 
-Global Instance sep_destruct_own p γ a b :
-  SepDestruct p (own γ (a ⋅ b)) (own γ a) (own γ b).
-Proof. apply sep_destruct_spatial. by rewrite own_op. Qed.
+Global Instance sep_destruct_own p γ a b1 b2 :
+  OpDestruct a b1 b2 → SepDestruct p (own γ a) (own γ b1) (own γ b2).
+Proof. rewrite /OpDestruct /SepDestruct => ->. by rewrite own_op. Qed.
 Global Instance sep_split_own γ a b :
   SepSplit (own γ (a ⋅ b)) (own γ a) (own γ b) | 90.
 Proof. by rewrite /SepSplit own_op. Qed.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ed27be14a826d549d31fc2999e2fc3e909991f50..119306c5502037bedebff74f68425b902d80bafa 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -768,3 +768,4 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
+Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e82db494ee5000c2f4192d9e1c491a6a51869374..d0d7d4eecb175976e45f9834cbd8815868ba57d0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -67,9 +67,9 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
   (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
 Proof.
   iIntros "H1 H2".
-  iRewrite (uPred.eq_sym x x with "[#]"). iApply uPred.eq_refl.
+  iRewrite (uPred.eq_sym x x with "[#]"); first done.
   iRewrite -("H1" $! _ with "[#]"); first done.
-  iApply uPred.eq_refl.
+  done.
 Qed.
 
 Lemma demo_6 (M : ucmraT) (P Q : uPred M) :