diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0928ff2d5f593868b645022683ba3bb8eb1c91a5..892d66b269ff4652f4f606fbc6ffbe6e2f82094e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,7 +4,8 @@ API-breaking change is listed.
 ## std++ 1.2.1 (unreleased)
 
 This release of std++ received contributions by Michael Sammler, Paolo
-G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, and Rodolphe Lepigre.
+G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, Rodolphe Lepigre and
+Paulo Emílio de Vilhena.
 
 Noteworthy additions and changes:
 
@@ -12,7 +13,7 @@ Noteworthy additions and changes:
 - Make `solve_ndisj` tactic more powerful.
 - Add typeclass `Involutive`.
 - Improved `naive_solver` performance in case the goal is trivially solvable.
-- A bunch of new lemmas for list operations.
+- A bunch of new lemmas for list, set, and map operations.
 - `lookup_imap` renamed into `map_lookup_imap`.
 
 ## std++ 1.2.0 (released 2019-04-26)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a323021d0d29704429405d293442150445a1846e..19251236bf22bf11a5de0270e4a9a0f75f4aaade 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1114,13 +1114,18 @@ Section map_filter.
       naive_solver.
   Qed.
 
-  Lemma map_filter_insert_not m i x :
-    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
+  Lemma map_filter_insert_not' m i x :
+    ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) →
+    filter P (<[i:=x]> m) = filter P m.
   Proof.
-    intros HP. apply map_filter_lookup_eq. intros j y Hy.
-    by rewrite lookup_insert_ne by naive_solver.
+    intros Hx HP. apply map_filter_lookup_eq. intros j y Hy.
+    rewrite lookup_insert_Some. naive_solver.
   Qed.
 
+  Lemma map_filter_insert_not m i x :
+    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
+  Proof. intros HP. by apply map_filter_insert_not'. Qed.
+
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
     apply map_eq. intros j. apply option_eq; intros y.
@@ -1139,6 +1144,16 @@ Section map_filter.
 
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
   Proof. apply map_fold_empty. Qed.
+
+  Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
+  Proof.
+    apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
+    { by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. }
+    rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)).
+    - rewrite map_filter_insert by done.
+      by rewrite map_to_list_insert, IH by (rewrite map_filter_lookup_None; auto).
+    - by rewrite map_filter_insert_not' by naive_solver.
+  Qed.
 End map_filter.
 
 (** ** Properties of the [map_Forall] predicate *)
diff --git a/theories/gmap.v b/theories/gmap.v
index c98df62b9e2536e103f66408290b6c57646fbbeb..2edcb42d67b878e4a8177be589d69a9915c064ae 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -279,6 +279,13 @@ Section gset.
     - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
     - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
   Qed.
+  Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
+    dom _ (gset_to_gmap x X) = X.
+  Proof.
+    induction X as [| y X not_in IH] using set_ind_L.
+    - rewrite gset_to_gmap_empty, dom_empty_L; done.
+    - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
+  Qed.
 End gset.
 
 Typeclasses Opaque gset.
diff --git a/theories/list.v b/theories/list.v
index 18365ab4e5859647d0662284b67273837158a977..dc522408f786b46b1b9839d6b99334943899a348 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -668,6 +668,42 @@ Proof.
   revert i j. induction k; intros i j ?; simpl;
     rewrite 1?list_insert_commute by lia; auto with f_equal.
 Qed.
+Lemma list_inserts_app_l l1 l2 l3 i :
+  list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
+Proof.
+  revert l1 i; induction l1 as [|x l1 IH]; [done|].
+  intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia.
+Qed.
+Lemma list_inserts_app_r l1 l2 l3 i :
+  list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
+Proof.
+  revert l1 i; induction l1 as [|x l1 IH]; [done|].
+  intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r.
+Qed.
+Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
+Proof.
+  revert i; induction l1 as [|x l1 IH]; [done|].
+  intro i. simpl. by rewrite IH.
+Qed.
+Lemma list_inserts_cons l1 l2 i x :
+  list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
+Proof.
+  revert i; induction l1 as [|y l1 IH]; [done|].
+  intro i. simpl. by rewrite IH.
+Qed.
+Lemma list_inserts_0_r l1 l2 l3 :
+  length l1 = length l2 → list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
+Proof.
+  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|].
+  rewrite list_inserts_cons. simpl. by rewrite IH.
+Qed.
+Lemma list_inserts_0_l l1 l2 l3 :
+  length l1 = length l3 → list_inserts 0 (l1 ++ l2) l3 = l1.
+Proof.
+  revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=.
+  { by rewrite list_inserts_nil. }
+  rewrite list_inserts_cons. simpl. by rewrite IH.
+Qed.
 
 (** ** Properties of the [elem_of] predicate *)
 Lemma not_elem_of_nil x : x ∉ [].