diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 5df84b2883e8098896000b727a2738f88011d7b0..cb296d38ea62388864206138e5ed44b14dc0be8c 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -671,6 +671,12 @@ Proof.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   - by rewrite !map_of_to_list.
 Qed.
+Lemma map_to_list_contains {A} (m1 m2 : M A) :
+  m1 ⊆ m2 → map_to_list m1 `contains` map_to_list m2.
+Proof.
+  intros; apply NoDup_contains; auto using NoDup_map_to_list.
+  intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
+Qed.
 Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
 Proof. done. Qed.
 Lemma map_of_list_cons {A} (l : list (K * A)) i x :