List countable instance is exponential

The countable instance for lists is exponential. This is slowing things down in some of my example calculations a lot. For example,

Time Compute ((empty : gmap (list (list nat)) nat) !! [[23]]).

takes 4 seconds on my machine. With higher numbers it easily runs out of memory. I am not able to open a merge request in this repo, but here is an implementation that is linear. It works by duplicating the bits of the encodings of each element and then indicating separators with two distinct bits.

Section list_countable.
  Context `{Countable A}.

  Fixpoint encode_single (p acc : positive) : positive :=
    match p with
    | 1 => acc
    | p'~0 => encode_single p' (acc~0~0)
    | p'~1 => encode_single p' (acc~1~1)
    end.

  Fixpoint encode_list' (l : list A) (acc : positive) : positive :=
    match l with
    | [] => acc
    | hd :: tl => encode_list' tl (encode_single (encode hd) (acc~1~0))
    end.

  Definition encode_list l := encode_list' l 1.

  Fixpoint decode_list'
           (p : positive)
           (acc_l : list A)
           (acc_elm : positive)
    : option (list A) :=
      match p with
      | 1 => Some acc_l
      | p'~0~0 => decode_list' p' acc_l (acc_elm~0)
      | p'~1~1 => decode_list' p' acc_l (acc_elm~1)
      | p'~1~0 => elm ← decode acc_elm;
                  decode_list' p' (elm :: acc_l) 1
      | _ => None
      end.

  Definition decode_list (p : positive) : option (list A) :=
    decode_list' p [] 1.

  Lemma encode_single_app (p acc : positive) :
    encode_single p acc = acc ++ encode_single p 1.
  Proof.
    generalize dependent acc.
    induction p.
    - intros acc.
      simpl.
      rewrite IHp.
      rewrite (IHp 7).
      rewrite Papp_assoc.
      reflexivity.
    - intros acc.
      simpl.
      rewrite IHp.
      rewrite (IHp 4).
      rewrite Papp_assoc.
      reflexivity.
    - intros acc.
      reflexivity.
  Qed.

  Lemma encode_list'_app (l : list A) (acc : positive) :
    encode_list' l acc = acc ++ encode_list' l 1.
  Proof.
    generalize dependent acc.
    induction l as [| hd tl IHl].
    - intros acc; reflexivity.
    - intros acc.
      simpl.
      rewrite IHl.
      rewrite (IHl (encode_single _ _)).
      rewrite Papp_assoc.
      rewrite (encode_single_app _ 6).
      rewrite Papp_assoc.
      simpl.
      rewrite <- encode_single_app.
      reflexivity.
  Qed.

  Lemma decode_list'_single (p prefix : positive) (l : list A) :
    decode_list' (prefix ++ encode_single p 1) l 1 = decode_list' prefix l p.
  Proof.
    generalize dependent prefix.
    induction p.
    - intros.
      simpl.
      rewrite encode_single_app.
      rewrite Papp_assoc.
      rewrite IHp.
      reflexivity.
    - intros.
      simpl.
      rewrite encode_single_app.
      rewrite Papp_assoc.
      rewrite IHp.
      reflexivity.
    - reflexivity.
  Qed.

  Lemma decode_list'_list (prefix : positive) (l acc : list A) :
    decode_list' (prefix ++ encode_list' l 1) acc 1 = decode_list' prefix (l ++ acc) 1.
  Proof.
    generalize dependent prefix.
    generalize dependent acc.
    induction l as [| hd tl IHl].
    - reflexivity.
    - intros acc prefix.
      simpl.
      rewrite encode_list'_app.
      rewrite Papp_assoc.
      rewrite IHl.
      rewrite encode_single_app.
      rewrite Papp_assoc.
      rewrite decode_list'_single.
      simpl.
      rewrite decode_encode.
      reflexivity.
  Qed.

  Global Program Instance list_countable : Countable (list A) :=
    {| encode := encode_list; decode := decode_list; |}.
  Next Obligation.
    intros l.
    unfold encode_list, decode_list.
    replace (encode_list' _ _) with (1 ++ encode_list' l 1) by apply Papp_1_l.
    rewrite decode_list'_list.
    simpl.
    rewrite app_nil_r.
    reflexivity.
  Qed.
End list_countable.

It is not as concise as any of your stuff so probably it needs some stylistic conversion. Also there's some specific lemmas stated for the representation of your instance which I have not shown for this one, so I don't know if you can even use this.