diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index eb51e26c06d97cad0fd5aeeb41b8c9049d507d93..991b01a286c06ad72e93c9aeddb6cf3f1fa0c464 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -156,6 +156,13 @@ Proof.
   intros m1 m2 EQm. apply elem_of_equiv. intros i.
   rewrite !elem_of_dom, EQm. done.
 Qed.
+Lemma dom_list_to_map {A} (l : list (K * A)) :
+  dom D (list_to_map l : M A) ≡ list_to_set l.*1.
+Proof.
+  induction l as [|?? IH].
+  - by rewrite dom_empty.
+  - simpl. by rewrite dom_insert, IH.
+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. *)
@@ -197,6 +204,9 @@ Section leibniz.
     (∀ 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.
+  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.
 End leibniz.
 
 (** * Set solver instances *)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 4d739220145a7d923276205f01b504e92a1f831b..b86876679f96b59dc1d1cb279cc0066639776f9b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -836,8 +836,15 @@ Qed.
 Lemma list_to_map_nil {A} : list_to_map [] = (∅ : M A).
 Proof. done. Qed.
 Lemma list_to_map_cons {A} (l : list (K * A)) i x :
-  list_to_map ((i, x) :: l) = <[i:=x]>(list_to_map l : M A).
+  list_to_map ((i, x) :: l) =@{M A} <[i:=x]>(list_to_map l).
 Proof. done. Qed.
+Lemma list_to_map_snoc {A} (l : list (K * A)) i x :
+  i ∉ l.*1 → list_to_map (l ++ [(i, x)]) =@{M A} <[i:=x]>(list_to_map l).
+Proof.
+  induction l as [|[k y] l IH]; [done|]. csimpl.
+  intros [Hneq Hni]%not_elem_of_cons.
+  by rewrite (IH Hni), insert_commute by done.
+Qed.
 Lemma list_to_map_fmap {A B} (f : A → B) l :
   list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).
 Proof.