diff --git a/CHANGELOG.md b/CHANGELOG.md
index a685028c775bf73fd0db65ff8ee0ed6d611e4f8d..516c417e0685b50c84f93f8f63eebf310764ac48 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,7 +14,6 @@ API-breaking change is listed.
 - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
 - Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
-  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
 - Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
   `StronglySorted_app_2`. Rename lemmas
   `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
@@ -28,6 +27,7 @@ Note that the script is not idempotent, do not run it twice.
 sed -i -E -f- $(find theories -name "*.v") <<EOF
 # length
 s/\bmap_filter_empty_iff\b/map_empty_filter/g
+# StronglySorted
 s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
 s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
 EOF
diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index 57f050a762987039eb1f409b95ebf803066d9ae3..f1f787f2787a852fccb725f59e9e97aa7f242293 100644
--- a/stdpp/sorting.v
+++ b/stdpp/sorting.v
@@ -1,7 +1,8 @@
 (** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
-From stdpp Require Export orders list sets.
+From stdpp Require Export orders list.
+From stdpp Require Import sets.
 From stdpp Require Import options.
 
 Section merge_sort.