diff --git a/prelude/gmap.v b/prelude/gmap.v
index dfb504396590fe514ae7d64a5d9a0303ad236745..2db7ae45d7311aa869340d98bf2aefbd1ef38402 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -112,6 +112,16 @@ Proof.
     by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
 Qed.
 
+Program Instance gmap_countable
+    `{Countable K, Countable A} : Countable (gmap K A) := {
+  encode m := encode (map_to_list m : list (K * A));
+  decode p := map_of_list <$> decode p
+}.
+Next Obligation.
+  intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
+  by rewrite map_of_to_list.
+Qed.
+
 (** * Finite sets *)
 Notation gset K := (mapset (gmap K)).
 Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
diff --git a/prelude/pmap.v b/prelude/pmap.v
index a558d72c65aa546f25266ac2f3b27c4e043bfd7b..a8edba1cb6857840fcf33b53476b6a595c625620 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -8,7 +8,7 @@ However, we extend Leroy's implementation by packing the trees into a Sigma
 type such that canonicity of representation is ensured. This is necesarry for
 Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
-From iris.prelude Require Import mapset.
+From iris.prelude Require Import mapset countable.
 From iris.prelude Require Export fin_maps.
 
 Local Open Scope positive_scope.
@@ -300,11 +300,19 @@ Proof.
   - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
 Qed.
 
+Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
+  encode m := encode (map_to_list m : list (positive * A));
+  decode p := map_of_list <$> decode p
+}.
+Next Obligation.
+  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite map_of_to_list.
+Qed.
+
 (** * Finite sets *)
 (** We construct sets of [positives]s satisfying extensional equality. *)
 Notation Pset := (mapset Pmap).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
-Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
+Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
 
 (** * Fresh numbers *)
 Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=