diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 666bb3b7cd5b8dda54941c64faa3d0fa065945a7..b639d50b47bcbd5f8844f08a9914f94d5566e1cf 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -3457,6 +3457,10 @@ 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.
 
+Lemma fmap_foldr_delete {A B} (f : A → B) (m : M A) is :
+  f <$> foldr delete m is = foldr delete (f <$> m) is.
+Proof. induction is; simpl; [done|]. rewrite fmap_delete. by f_equal. Qed.
+
 (** ** Properties of the folding the [delete] function over a set *)
 Section set_fold.
   Context `{FinSet K C}.
@@ -3536,6 +3540,10 @@ Section set_fold.
     - intros. by rewrite delete_idemp.
     - intros. by rewrite delete_commute.
   Qed.
+
+  Lemma fmap_set_fold_delete {A B} (f : A → B) (m : M A) X :
+    f <$> set_fold delete m X = set_fold delete (f <$> m) X.
+  Proof. apply fmap_foldr_delete. Qed.
 End set_fold.
 
 (** ** Misc properties about the order *)