diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 508b0905eab29bfeabfb69393b4b32ad6286f396..666bb3b7cd5b8dda54941c64faa3d0fa065945a7 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -3457,6 +3457,87 @@ Lemma foldr_delete_intersection {A} (m1 m2 : M A) is :
   foldr delete (m1 ∩ m2) is = foldr delete m1 is ∩ foldr delete m2 is.
 Proof. apply foldr_delete_intersection_with. Qed.
 
+(** ** Properties of the folding the [delete] function over a set *)
+Section set_fold.
+  Context `{FinSet K C}.
+  Implicit Types X Y : C.
+
+  Lemma set_fold_delete_empty {A} X : set_fold delete ∅ X =@{M A} ∅.
+  Proof. apply foldr_delete_empty. Qed.
+
+  Lemma lookup_set_fold_delete {A} (m : M A) X j :
+    j ∈ X → set_fold delete m X !! j = None.
+  Proof. intros. apply lookup_foldr_delete. set_solver. Qed.
+  Lemma lookup_set_fold_delete_not_elem_of {A} (m : M A) X j :
+    j ∉ X → set_fold delete m X !! j = m !! j.
+  Proof. intros. apply lookup_foldr_delete_not_elem_of. set_solver. Qed.
+  Lemma lookup_set_fold_delete_Some {A} (m : M A) X j y :
+    set_fold delete m X !! j = Some y ↔ j ∉ X ∧ m !! j = Some y.
+  Proof. rewrite <-elem_of_elements. apply lookup_foldr_delete_Some. Qed.
+
+  Lemma set_fold_delete_notin {A} (m : M A) X :
+    set_Forall (λ i, m !! i = None) X → set_fold delete m X = m.
+  Proof. intros. by apply foldr_delete_notin, set_Forall_elements. Qed.
+
+  Lemma set_fold_delete_commute {A} (m : M A) X j :
+    delete j (set_fold delete m X) = set_fold delete (delete j m) X.
+  Proof. apply foldr_delete_commute. Qed.
+  Lemma set_fold_delete_insert {A} (m : M A) X j x :
+    j ∈ X → set_fold delete (<[j:=x]> m) X = set_fold delete m X.
+  Proof. intros. apply foldr_delete_insert. set_solver. Qed.
+  Lemma set_fold_delete_insert_ne {A} (m : M A) X j x :
+    j ∉ X → set_fold delete (<[j:=x]> m) X = <[j:=x]> (set_fold delete m X).
+  Proof. intros. apply foldr_delete_insert_ne. set_solver. Qed.
+
+  Lemma set_fold_delete_subseteq {A} (m : M A) X : set_fold delete m X ⊆ m.
+  Proof. apply foldr_delete_subseteq. Qed.
+
+  Lemma map_Forall_set_fold_delete {A} (P : K → A → Prop) (m : M A) X :
+    map_Forall P m → map_Forall P (set_fold delete m X).
+  Proof. apply map_Forall_foldr_delete. Qed.
+  Lemma map_Exists_set_fold_delete {A} (P : K → A → Prop) (m : M A) X :
+    map_Exists P (set_fold delete m X) → map_Exists P m.
+  Proof. apply map_Exists_foldr_delete. Qed.
+
+  Lemma map_disjoint_set_fold_delete_l {A} (m1 m2 : M A) X :
+    m1 ##ₘ m2 → set_fold delete m1 X ##ₘ m2.
+  Proof. eauto using map_disjoint_weaken_l, set_fold_delete_subseteq. Qed.
+  Lemma map_disjoint_set_fold_delete_r {A} (m1 m2 : M A) X :
+    m1 ##ₘ m2 → m1 ##ₘ set_fold delete m2 X.
+  Proof. eauto using map_disjoint_weaken_r, set_fold_delete_subseteq. Qed.
+
+  Lemma map_agree_set_fold_delete_l {A} (m1 m2 : M A) X :
+    map_agree m1 m2 → map_agree (set_fold delete m1 X) m2.
+  Proof. eauto using map_agree_weaken_l, set_fold_delete_subseteq. Qed.
+  Lemma map_agree_set_fold_delete_r {A} (m1 m2 : M A) X :
+    map_agree m1 m2 → map_agree m1 (set_fold delete m2 X).
+  Proof. eauto using map_agree_weaken_r, set_fold_delete_subseteq. Qed.
+
+  Lemma set_fold_delete_union_with {A} (f : A → A → option A) (m1 m2 : M A) X :
+    set_fold delete (union_with f m1 m2) X =
+      union_with f (set_fold delete m1 X) (set_fold delete m2 X).
+  Proof. apply foldr_delete_union_with. Qed.
+  Lemma set_fold_delete_union {A} (m1 m2 : M A) X :
+    set_fold delete (m1 ∪ m2) X = set_fold delete m1 X ∪ set_fold delete m2 X.
+  Proof. apply set_fold_delete_union_with. Qed.
+
+  Lemma set_fold_delete_intersection_with {A} (f : A → A → option A) (m1 m2 : M A) X :
+    set_fold delete (intersection_with f m1 m2) X =
+      intersection_with f (set_fold delete m1 X) (set_fold delete m2 X).
+  Proof. apply foldr_delete_intersection_with. Qed.
+  Lemma set_fold_delete_intersection {A} (m1 m2 : M A) X :
+    set_fold delete (m1 ∩ m2) X = set_fold delete m1 X ∩ set_fold delete m2 X.
+  Proof. apply set_fold_delete_intersection_with. Qed.
+
+  Lemma set_fold_delete_set_union {A} (m : M A) X1 X2 :
+    set_fold delete m (X1 ∪ X2) = set_fold delete (set_fold delete m X1) X2.
+  Proof.
+    apply (set_fold_union_strong eq); [solve_proper|..].
+    - intros. by rewrite delete_idemp.
+    - intros. by rewrite delete_commute.
+  Qed.
+End set_fold.
+
 (** ** Misc properties about the order *)
 Lemma map_subseteq_inv {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ⊂ m2 ∨ m1 = m2.
 Proof.