diff --git a/theories/list.v b/theories/list.v
index d0c27ab3e3487f7f8193776937f3a17b41d0145f..73991db93ed75c4a893dcf738f968c19666159c2 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -473,6 +473,8 @@ Proof.
   intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
   rewrite Hi at 1. by apply alter_app_r.
 Qed.
+Lemma list_alter_id f l i : (∀ x, f x = x) → alter f i l = l.
+Proof. intros ?. revert i. induction l; intros [|?]; f_equal'; auto. Qed.
 Lemma list_alter_ext f g l k i :
   (∀ x, l !! i = Some x → f x = g x) → l = k → alter f i l = alter g i k.
 Proof. intros H ->. revert i H. induction k; intros [|?] ?; f_equal'; auto. Qed.
diff --git a/theories/nmap.v b/theories/nmap.v
index 5f78de7a348ab798d96b2521044d28ca49e54ce4..b66ed43b7d5fedbf54b88b1ac2b0871d120389fb 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -21,6 +21,7 @@ Proof.
   end; abstract congruence.
 Defined.
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
+Global Opaque Nempty.
 Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
   match i with
   | N0 => Nmap_0 t