diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 243b1644b5088383ef52440c5fa071bbadd43aae..ed3c554e38b2d71962b07052849772b8841da78f 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -35,6 +35,20 @@ Proof.
   destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists.
 Qed.
 
+Lemma dom_imap_subseteq {A B} (f: K → A → option B) (m: M A) :
+  dom D (map_imap f m) ⊆ dom D m.
+Proof.
+  intros k. rewrite 2!elem_of_dom, map_lookup_imap.
+  destruct 1 as [?[?[Eq _]]%bind_Some]. by eexists.
+Qed.
+Lemma dom_imap {A B} (f: K → A → option B) (m: M A) X :
+  (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
+  dom D (map_imap f m) ≡ X.
+Proof.
+  intros HX k. rewrite elem_of_dom, HX, map_lookup_imap.
+  unfold is_Some. setoid_rewrite bind_Some. naive_solver.
+Qed.
+
 Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m.
 Proof. rewrite elem_of_dom; eauto. Qed.
 Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None.
@@ -167,6 +181,10 @@ Section leibniz.
   Proof. unfold_leibniz; apply dom_difference. Qed.
   Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
   Proof. unfold_leibniz; apply dom_fmap. Qed.
+  Lemma dom_imap_L {A B} (f: K → A → option B) (m: M A) X :
+    (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
+    dom D (map_imap f m) = X.
+  Proof. unfold_leibniz; apply dom_imap. Qed.
 End leibniz.
 
 (** * Set solver instances *)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 447b6751a052cb5e272fea91da58f8d08ef662b6..3091d8389893326c5aefcb638a122f3336057a25 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -944,6 +944,16 @@ Proof.
       by rewrite map_lookup_imap.
 Qed.
 
+Lemma map_imap_delete {A B} (f : K → A → option B) (m : M A) (i : K) :
+  map_imap f (delete i m) = delete i (map_imap f m).
+Proof.
+  apply map_eq. intros k. rewrite map_lookup_imap.
+  destruct (decide (k = i)) as [->|Hk_not_i].
+  - by rewrite !lookup_delete.
+  - rewrite !lookup_delete_ne by done.
+    by rewrite map_lookup_imap.
+Qed.
+
 Lemma map_imap_ext {A1 A2 B} (f1 : K → A1 → option B)
     (f2 : K → A2 → option B) (m1 : M A1) (m2 : M A2) :
   (∀ k, f1 k <$> (m1 !! k) = f2 k <$> (m2 !! k)) →
@@ -953,6 +963,17 @@ Proof.
   specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 
+Lemma map_imap_compose {A1 A2 B} (f1 : K → A1 → option B)
+    (f2 : K → A2 → option A1) (m : M A2) :
+  map_imap f1 (map_imap f2 m) = map_imap (λ k x, f2 k x ≫= f1 k) m.
+Proof.
+  apply map_eq. intros i. rewrite !map_lookup_imap. by destruct (m !! i).
+Qed.
+
+Lemma map_imap_empty {A B} (f : K → A → option B) :
+  map_imap f ∅ =@{M B} ∅.
+Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
+
 (** ** Properties of the size operation *)
 Lemma map_size_empty {A} : size (∅ : M A) = 0.
 Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.