diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 01d97b757819dc562af34bee7ca915f02aa0e4e2..3a5cbe52a1b8384ff7293c7c8a28de9911b37939 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -45,7 +45,10 @@ Global Instance gmapO_leibniz: LeibnizEquiv A → LeibnizEquiv gmapO.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
 
 Global Instance lookup_ne k : NonExpansive (lookup k : gmap K A → option A).
-Proof. by intros m1 m2. Qed.
+Proof. by intros n m1 m2. Qed.
+Global Instance lookup_total_ne `{!Inhabited A} k :
+  NonExpansive (lookup_total k : gmap K A → A).
+Proof. intros n m1 m2. rewrite !lookup_total_alt. by intros ->. Qed.
 Global Instance partial_alter_ne n :
   Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n)
          (partial_alter (M:=gmap K A)).
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 492ffe0b37e0d15fd97f44796f0174757d19ad7e..a6d5d0f9289cad342f44f1cbb457c607c7c44835 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -23,6 +23,9 @@ Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
 Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
 Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Global Instance list_lookup_total_ne `{!Inhabited A} i :
+  NonExpansive (lookup_total (M:=list A) i).
+Proof. intros ???. rewrite !list_lookup_total_alt. by intros ->. Qed.
 Global Instance list_alter_ne n f i :
   Proper (dist n ==> dist n) f →
   Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.