diff --git a/tests/gmap.ref b/tests/gmap.ref
index a4d42549233b5c0153c1b455eb21f2651d09f7d4..afb49b4c188b4136f0563e6a53c524778e8818db 100644
--- a/tests/gmap.ref
+++ b/tests/gmap.ref
@@ -70,3 +70,11 @@ Failed to progress.
   
   ============================
   bool_decide (∅ ⊆ {[1; 2; 3]}) = true
+1 goal
+  
+  ============================
+  {[3 := false; 2 := true]} = {[2 := true; 3 := false]}
+1 goal
+  
+  ============================
+  Some true = Some true
diff --git a/tests/gmap.v b/tests/gmap.v
index e8e90b6192214047038a9813c2cf2a670b79dbe7..4de79e14abe28055daecfbcd1fdcc142c0f385d4 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -1,4 +1,4 @@
-From stdpp Require Import gmap.
+From stdpp Require Import pmap gmap.
 
 Goal {[1; 2; 3]} =@{gset nat} ∅.
 Proof.
@@ -71,4 +71,15 @@ Qed.
 
 Theorem gmap_insert_comm :
   <[3:=false]> {[2:=true]} =@{gmap nat bool} <[2:=true]> {[3:=false]}.
-Proof. reflexivity. Qed.
+Proof.
+  simpl. Show.
+  reflexivity.
+Qed.
+
+Transparent gmap_empty.
+Arguments map_insert _ _ _ / _ _ _ _ : assert.
+Arguments Plookup _ _ _ / : assert.
+
+Theorem gmap_lookup_concrete :
+  lookup (M:=gmap nat bool) 2 (<[3:=false]> {[2:=true]}) = Some true.
+Proof. simpl. Show. reflexivity. Qed.