diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 2f74ff9c5dcb5595bd2b9efa4ddf707407cc484b..d5ed50970509f82e2dc27f5ab9af6cbe27d153c0 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -1,5 +1,5 @@
 From stdpp Require Export list gmap.
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export list cmra.
 From iris.algebra Require Import updates local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -97,6 +97,13 @@ Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 (** Internalized properties *)
 End ofe.
 
+Global Instance map_seq_ne {A : ofe} start :
+  NonExpansive (map_seq (M:=gmap nat A) start).
+Proof.
+  intros n l1 l2 Hl. revert start.
+  induction Hl; intros; simpl; repeat (done || f_equiv).
+Qed.
+
 Global Arguments gmapO _ {_ _} _.
 
 (** Non-expansiveness of higher-order map functions and big-ops *)