diff --git a/tests/maps.v b/tests/maps.v
index e45e235ed434fddf4268ea1a38fc0f29ca89dc4f..33bd5b693616a47902c216a08b8670afc6353d82 100644
--- a/tests/maps.v
+++ b/tests/maps.v
@@ -302,3 +302,52 @@ Proof.
     | GTest ts1, GTest ts2 => cast_if (decide (ts1 = ts2))
     end); abstract congruence.
 Defined.
+
+(** We show that [gtest K] is countable itself. This means that we can use
+[gtest K] (which involves nested uses of [gmap]) as keys in [gmap]/[gset], i.e.,
+[gmap (gtest K) V] and [gset (gtest K)]. And even [gtest (gtest K)].
+
+Showing that [gtest K] is countable is not trivial due to its nested-inductive
+nature. We need to write [encode] and [decode] functions, and prove that they
+are inverses. We do this by converting to/from [gen_tree]. This shows that Coq's
+guardedness checker accepts non-trivial recursive definitions involving [gtest],
+and we can do non-trivial induction proofs about [gtest]. *)
+Global Program Instance gtest_countable `{Countable K} : Countable (gtest K) :=
+  let enc :=
+    fix go t :=
+      let 'GTest ts := t return _ in
+      GenNode 0 (map_fold (λ (k : K) t rec, GenLeaf k :: go t :: rec) [] ts) in
+  let dec_list := λ dec : gen_tree K → gtest K,
+    fix go ts :=
+      match ts return gmap K (gtest K) with
+      | GenLeaf k :: t :: ts => <[k:=dec t]> (go ts)
+      | _ => ∅
+      end in
+  let dec :=
+    fix go t :=
+      match t return _ with
+      | GenNode 0 ts => GTest (dec_list go ts)
+      | _ => GTest ∅ (* dummy *)
+      end in
+  inj_countable' enc dec _.
+Next Obligation.
+  intros K ?? enc dec_list dec t.
+  remember (gtest_size t) as n eqn:Hn. revert t Hn.
+  induction (lt_wf n) as [n _ IH]; intros [ts] ->; simpl in *; f_equal.
+  revert ts IH. apply (map_fold_ind (λ r ts, _ → dec_list dec r = ts)); [done|].
+  intros i t ts r ? IHts IHt; simpl. f_equal.
+  - eapply IHt; [|done]. rewrite map_fold_insert_L by auto with lia. lia.
+  - apply IHts; intros n ? t' ->. eapply IHt; [|done].
+    rewrite map_fold_insert_L by auto with lia. lia.
+Qed.
+
+Goal
+  ({[ GTest {[ 1 := GTest ∅ ]} := "foo" ]} : gmap (gtest nat) string)
+  !! GTest {[ 1 := GTest ∅ ]} = Some "foo".
+Proof. reflexivity. Qed.
+
+Goal {[ GTest {[ 1 := GTest ∅ ]} ]} ≠@{gset (gtest nat)} {[ GTest ∅ ]}.
+Proof. discriminate. Qed.
+
+Goal GTest {[ GTest {[ 1 := GTest ∅ ]} := GTest ∅ ]} ≠@{gtest (gtest nat)} GTest ∅.
+Proof. discriminate. Qed.