diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a5aa829ce4f04384ab01e23e7db4d3871b24f51c..bfbc2eebfb5f97344475e5fc6239650d9b16c902 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -567,6 +567,13 @@ Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
 Proof.
   intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono.
 Qed.
+Lemma insert_subseteq_l {A} (m1 m2 : M A) i x :
+  m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
+Proof.
+  intros Hi Hincl. replace m2 with (<[i:=x]> m2).
+  - apply insert_mono. done.
+  - apply insert_id. done.
+Qed.
 
 Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :
   m1 !! i = None → <[i:=x]> m1 ⊆ m2 → m1 ⊆ delete i m2.