diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index c44ce9f34a1b98f7d0055f03093260e38178dca8..f0e3e9b1361e5d7976daea9245013125d247672a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -163,6 +163,41 @@ Proof.
   - by rewrite dom_empty.
   - simpl. by rewrite dom_insert, IH.
 Qed.
+
+Lemma dom_singleton_inv {A} (m : M A) i :
+  dom D m ≡ {[i]} → ∃ x, m = {[i := x]}.
+Proof.
+  intros Hdom. assert (is_Some (m !! i)) as [x ?].
+  { apply (elem_of_dom (D:=D)); set_solver. }
+  exists x. apply map_eq; intros j.
+  destruct (decide (i = j)); simplify_map_eq; [done|].
+  apply not_elem_of_dom. set_solver.
+Qed.
+
+Lemma dom_union_inv `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) :
+  X1 ## X2 →
+  dom D m ≡ X1 ∪ X2 →
+  ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom D m1 ≡ X1 ∧ dom D m2 ≡ X2.
+Proof.
+  intros.
+  exists (filter (λ '(k,x), k ∈ X1) m), (filter (λ '(k,x), k ∉ X1) m).
+  assert (filter (λ '(k, _), k ∈ X1) m ##ₘ filter (λ '(k, _), k ∉ X1) m).
+  { apply map_disjoint_filter. }
+  split_and!; [|done| |].
+  - apply map_eq; intros i. apply option_eq; intros x.
+    rewrite lookup_union_Some, !map_filter_lookup_Some by done.
+    destruct (decide (i ∈ X1)); naive_solver.
+  - apply dom_filter; intros i; split; [|naive_solver].
+    intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
+    naive_solver.
+  - apply dom_filter; intros i; split.
+    + intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
+      naive_solver.
+    + intros (x&?&?). apply dec_stable; intros ?.
+      assert (m !! i = None) by (apply not_elem_of_dom; set_solver).
+      naive_solver.
+Qed.
+
 (** If [D] has Leibniz equality, we can show an even stronger result.  This is a
 common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
 (and thus also [gset K], the usual domain) but the value type [A] does not. *)
@@ -207,6 +242,14 @@ Section leibniz.
   Lemma dom_list_to_map_L {A} (l : list (K * A)) :
     dom D (list_to_map l : M A) = list_to_set l.*1.
   Proof. unfold_leibniz. apply dom_list_to_map. Qed.
+  Lemma dom_singleton_inv_L {A} (m : M A) i :
+    dom D m = {[i]} → ∃ x, m = {[i := x]}.
+  Proof. unfold_leibniz. apply dom_singleton_inv. Qed.
+  Lemma dom_union_inv_L `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) :
+    X1 ## X2 →
+    dom D m = X1 ∪ X2 →
+    ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom D m1 = X1 ∧ dom D m2 = X2.
+  Proof. unfold_leibniz. apply dom_union_inv. Qed.
 End leibniz.
 
 (** * Set solver instances *)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 4e7ae1fc182056ac314a920fd8de4047f4f8827d..aa75c29d05ede015211e0b72cf98ee905b64a998 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -296,6 +296,8 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
 Proof.
   intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
 Qed.
+Lemma map_empty_subseteq {A} (m : M A) : ∅ ⊆ m.
+Proof. apply map_subseteq_spec. intros k v []%lookup_empty_Some. Qed.
 
 Lemma map_subset_alt {A} (m1 m2 : M A) :
   m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i).
@@ -1475,6 +1477,9 @@ Section merge.
   Context {A} (f : option A → option A → option A) `{!DiagNone f}.
   Implicit Types m : M A.
 
+  (** These instances can in many cases not be applied automatically due to Coq
+  unification bug #6294. Hence there are many explicit derived instances for
+  specific operations such as union or difference in the rest of this file. *)
   Global Instance: LeftId (=) None f → LeftId (=) (∅ : M A) (merge f).
   Proof.
     intros ??. apply map_eq. intros.
@@ -2104,6 +2109,20 @@ Qed.
 Lemma delete_union {A} (m1 m2 : M A) i :
   delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
 Proof. apply delete_union_with. Qed.
+Lemma union_delete_insert {A} (m1 m2 : M A) i x :
+  m1 !! i = Some x →
+  delete i m1 ∪ <[i:=x]> m2 = m1 ∪ m2.
+Proof.
+  intros. rewrite <-insert_union_r by apply lookup_delete.
+  by rewrite insert_union_l, insert_delete, insert_id by done.
+Qed.
+Lemma union_insert_delete {A} (m1 m2 : M A) i x :
+  m1 !! i = None → m2 !! i = Some x →
+  <[i:=x]> m1 ∪ delete i m2 = m1 ∪ m2.
+Proof.
+  intros. rewrite <-insert_union_l by apply lookup_delete.
+  by rewrite insert_union_r, insert_delete, insert_id by done.
+Qed.
 Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
   map_Forall P (m1 ∪ m2) → map_Forall P m1.
 Proof. intros HP i x ?. apply HP, lookup_union_Some_raw; auto. Qed.
@@ -2371,6 +2390,25 @@ Proof.
   apply map_empty; intros i. rewrite lookup_difference_None.
   destruct (m !! i); eauto.
 Qed.
+Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
+Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
+Proof. by rewrite (right_id _ _). Qed.
+
+Lemma delete_difference {A} (m1 m2 : M A) i x :
+  delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
+Proof.
+  apply map_eq. intros j. apply option_eq. intros y.
+  rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None.
+  naive_solver.
+Qed.
+Lemma difference_delete {A} (m1 m2 : M A) i x :
+  m1 !! i = Some x →
+  m1 ∖ delete i m2 = <[i:=x]> (m1 ∖ m2).
+Proof.
+  intros. apply map_eq. intros j. apply option_eq. intros y.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_delete_None.
+  destruct (decide (i = j)); naive_solver.
+Qed.
 End theorems.
 
 (** ** The seq operation *)
diff --git a/theories/sets.v b/theories/sets.v
index 6e5d84be44a85471bff399b6e2c3bf5e4fded0f4..f4b506889c3e0812fb7f0219e0108af9d3bc913a 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -779,6 +779,8 @@ Section set.
       intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
       destruct (decide (x ∈ X)); intuition.
     Qed.
+    Lemma union_difference_singleton x Y : x ∈ Y → Y ≡ {[x]} ∪ Y ∖ {[x]}.
+    Proof. intros ?. apply union_difference. set_solver. Qed.
     Lemma difference_union X Y : X ∖ Y ∪ Y ≡ X ∪ Y.
     Proof.
       intros x. rewrite !elem_of_union; rewrite elem_of_difference.
@@ -800,6 +802,8 @@ Section set.
     Context `{!LeibnizEquiv C}.
     Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
     Proof. unfold_leibniz. apply union_difference. Qed.
+    Lemma union_difference_singleton_L x Y : x ∈ Y → Y = {[x]} ∪ Y ∖ {[x]}.
+    Proof. unfold_leibniz. apply union_difference_singleton. Qed.
     Lemma difference_union_L X Y : X ∖ Y ∪ Y = X ∪ Y.
     Proof. unfold_leibniz. apply difference_union. Qed.
     Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅.