diff --git a/_CoqProject b/_CoqProject
index 5a389c306975fd587fbc98adc3c33bf94412bfbc..8e0851b1a8ffa53ce6adc95350c4587d7d65ad12 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -38,6 +38,7 @@ theories/logrel/term_typing_rules.v
 theories/logrel/session_typing_rules.v
 theories/logrel/napp.v
 theories/logrel/lib/mutex.v
+theories/logrel/lib/list.v
 theories/logrel/lib/par_start.v
 theories/logrel/examples/pair.v
 theories/logrel/examples/par_recv.v
diff --git a/papers/CPP21.md b/papers/CPP21.md
index 757dd284f4542667e85e90ccb28341c0e03fb246..151b50a870a4752e7b8021f7df944e1a60b86975 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -11,6 +11,8 @@
   instead of an n-ary rule with multiple premises.
 - The disjunction of the compute client list invariant is encoded using a boolean
   flag, as it makes mechanisation easier.
+- The mechanisation employs a typing judgement for values (`ltyped_val`),
+  for technical reasons.
 
 ## Examples
 
@@ -23,4 +25,5 @@
   This program sends computation requests and receives their results in parallel,
   analogous to the producer-consumer pattern. It uses a lock to share the channel
   and a shared counter, that keeps track of the number of computations in transit.
-  The computation service can be found in [theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v)
+  The computation service can be found in [theories/logrel/examples/compute_service.v](../theories/logrel/examples/compute_service.v). The definition of the list type
+  and the weakest precondition for `llength` can be found in [theories/logrel/lib/list.v](../theories/logrel/lib/list.v)
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 7a0c7e07b702171cf9efdd808074e147640d6439..bb7d648adf71fdb493ccbfb0ec4d8c8585f190ca 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -1,10 +1,26 @@
+(** This file contains an example of a client that uses the
+compute service of [theories/logrel/examples/compute_service.v]
+which has the type:
+
+  μ rec. & { cont : ? (X:★) (() ⊸ X). ! X. rec,
+             stop : end }
+
+It does so to compute the results of an input list with type
+[list (() ⊸A)], into a list with type [list A], sending the
+computations in parallel with receiving the results.
+
+The client cannot be type checked with the rules of the type system,
+as (1) its behaviour depends on the length of the list, and (2)
+it shares the channel endpoint which changes between concurrent accesses.
+Its typing judgement can however be manually verified, after which
+it is composed with the type checked service. *)
 From iris.algebra Require Import frac.
 From iris.heap_lang Require Import metatheory.
 From actris.utils Require Import llist.
 From actris.channel Require Import proofmode proto channel.
 From actris.logrel Require Import term_typing_rules session_typing_rules
      subtyping_rules napp.
-From actris.logrel.lib Require Import par_start.
+From actris.logrel.lib Require Import list par_start.
 From actris.logrel.examples Require Import compute_service.
 
 Definition send_all_par : val :=
@@ -40,15 +56,6 @@ Definition compute_client : val :=
    (send_all_par "c" "xs" "lk" "counter" |||
     recv_all_par "c" "ys" "n" "lk" "counter");; "ys".
 
-Definition lty_list_aux `{!heapG Σ} (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
-  ref_uniq (() + (A * X)).
-Instance lty_list_aux_contractive `{!heapG Σ} A :
-  Contractive (@lty_list_aux Σ _ A).
-Proof. solve_proto_contractive. Qed.
-Definition lty_list `{!heapG Σ} (A : ltty Σ) : ltty Σ := lty_rec (lty_list_aux A).
-
-Notation "'list' A" := (lty_list A) (at level 10) : lty_scope.
-
 Section compute_example.
   Context `{heapG Σ, chanG Σ, lockG Σ, spawnG Σ}.
   Context `{!inG Σ fracR}.
@@ -66,39 +73,6 @@ Section compute_example.
                 (lsty_car (compute_type_client_aux compute_type_client)).
   Proof. apply proto_unfold_eq, (fixpoint_unfold compute_type_client_aux). Qed.
 
-  Definition list_pred (A : ltty Σ) : val → val → iProp Σ :=
-    (λ v w : val, ⌜v = w⌝ ∗ ltty_car A v)%I.
-
-  Lemma llength_spec A (l : loc) :
-    ⊢ {{{ ltty_car (list A) #l }}} llength #l
-      {{{ xs (n:Z), RET #n; ⌜Z.of_nat (length xs) = n⌝ ∗
-                            llist (λ v w , ⌜v = w⌝ ∗ ltty_car A v) l xs }}}.
-  Proof.
-    iIntros "!>" (Φ) "Hl HΦ".
-    iLöb as "IH" forall (l Φ).
-    wp_lam.
-    rewrite {2}/lty_list /lty_rec /lty_list_aux fixpoint_unfold.
-    iDestruct "Hl" as (ltmp l' [=<-]) "[Hl [ Hl' | Hl' ]]".
-    - wp_load. iDestruct "Hl'" as (xs ->) "Hl'". wp_pures.
-      iAssert (llist (list_pred A) l [])%I with "[Hl Hl']" as "Hl".
-      { rewrite /llist. iDestruct "Hl'" as %->. iApply "Hl". }
-      iApply "HΦ". eauto with iFrame.
-    - wp_load. iDestruct "Hl'" as (xs ->) "Hl'". wp_pures.
-      iDestruct "Hl'" as (x vl' ->) "[HA Hl']".
-      (* iDestruct "Hl'" as (l' xs ->) "[Hl' Hl'']". *)
-      wp_pures.
-      rewrite fixpoint_unfold.
-      iDestruct "Hl'" as (l' xs ->) "[Hl' Hl'']".
-      wp_apply ("IH" with "[Hl' Hl'']").
-      { rewrite /lty_list /lty_rec.
-        iEval (rewrite fixpoint_unfold).
-        iExists _, _. iFrame "Hl' Hl''". done. }
-      iIntros (ys n) "[<- H]".
-      iAssert (llist (list_pred A) l (x :: ys))%I with "[Hl HA H]" as "Hl".
-      { iExists x, l'. eauto with iFrame. }
-      wp_pures. iApply "HΦ". iFrame "Hl". by rewrite (Nat2Z.inj_add 1).
-  Qed.
-
   Definition cont_type (A : ltty Σ) : lsty Σ :=
     (lty_select (<[ cont := <!!> TY () ⊸ A ; END ]>∅))%lty.
   Definition stop_type : lsty Σ :=
@@ -186,10 +160,10 @@ Section compute_example.
   Qed.
 
   Lemma send_all_par_spec γ γf A c l xs lk counter :
-    {{{ llist (list_pred (() ⊸ A)) l xs ∗ own γf 1%Qp ∗
+    {{{ llist (llist_type_pred (() ⊸ A)) l xs ∗ own γf 1%Qp ∗
         is_lock γ lk (compute_type_invariant γf A c counter) }}}
       send_all_par c #l lk #counter
-    {{{ RET #(); llist (list_pred (() ⊸ A)) l [] ∗
+    {{{ RET #(); llist (llist_type_pred (() ⊸ A)) l [] ∗
                  is_lock γ lk (compute_type_invariant γf A c counter) }}}.
   Proof.
     iIntros (Φ) "(Hl & Hf & #Hlk) HΦ".
@@ -256,11 +230,11 @@ Section compute_example.
   Qed.
 
   Lemma recv_all_par_spec γ γf A c l n lk counter :
-    {{{ llist (list_pred A) l [] ∗
+    {{{ llist (llist_type_pred A) l [] ∗
         is_lock γ lk (compute_type_invariant γf A c counter) }}}
       recv_all_par c #l #n lk #counter
     {{{ ys, RET #(); ⌜n = length ys⌝ ∗
-                     llist (list_pred A) l ys ∗
+                     llist (llist_type_pred A) l ys ∗
                      is_lock γ lk (compute_type_invariant γf A c counter)  }}}.
   Proof.
     iIntros (Φ) "(Hl & #Hlk) HΦ".
@@ -294,25 +268,6 @@ Section compute_example.
     iPureIntro. by rewrite Heq.
   Qed.
 
-  Lemma llist_lty_list lys ys A :
-    llist (list_pred A) lys ys -∗
-    ltty_car (lty_list A) #lys.
-  Proof.
-    iIntros "Hlys".
-    iInduction ys as [|y ys] "IH" forall (lys).
-    - rewrite /lty_list /lty_rec fixpoint_unfold.
-      iExists lys, NONEV. rewrite /llist. iFrame "Hlys".
-      iSplit; [ done | ].
-      iLeft. eauto.
-    - iDestruct "Hlys" as (vb l'') "[[-> HB] [Hl' Hrec]]".
-      iEval (rewrite /lty_list /lty_rec fixpoint_unfold).
-      iExists lys, _. iFrame "Hl'".
-      iSplit; [ done | ].
-      rewrite /lty_list /lty_rec.
-      iRight. iExists _. iSplit; [ done | ]. iExists _, _. iSplit; [ done | ].
-      iFrame "HB". by iApply ("IH" with "Hrec").
-  Qed.
-
   Lemma ltyped_compute_client Γ (A : ltty Σ) :
     ⊢ Γ ⊨ compute_client : lty_list (() ⊸ A) ⊸
                            chan compute_type_client ⊸
@@ -341,7 +296,7 @@ Section compute_example.
     iIntros (lk γ) "#Hlk".
     wp_apply (par_spec
                 (λ v, ⌜v = #()⌝)%I
-                (λ v, ∃ ys, ⌜v = #()⌝ ∗ llist (list_pred A) lys ys)%I
+                (λ v, ∃ ys, ⌜v = #()⌝ ∗ llist (llist_type_pred A) lys ys)%I
                 with "[Hlxs Hf] [Hlys]").
     { wp_apply (send_all_par_spec with "[$Hlxs $Hf $Hlk]").
       iIntros "(Hlxs & _)". eauto. }
diff --git a/theories/logrel/examples/compute_service.v b/theories/logrel/examples/compute_service.v
index a83fea1865cbc68ab42ab4cdae63dc6e8dbd8887..adcc7a6d56c2cb6ee5314048e473e9b18365cfb3 100644
--- a/theories/logrel/examples/compute_service.v
+++ b/theories/logrel/examples/compute_service.v
@@ -1,3 +1,10 @@
+(** This file contains a computation service with the type
+
+  μ rec. & { cont : ? (X:★) (() ⊸ X). ! X. rec,
+             stop : end }
+
+It recursively receives computations, computes them, and then
+sends back the results. *)
 From iris.algebra Require Import frac.
 From iris.heap_lang Require Import metatheory.
 From actris.utils Require Import llist.
diff --git a/theories/logrel/examples/mapper_list.v b/theories/logrel/examples/mapper_list.v
index eb78821c155d995f3054b248dbe4a0e05edf5dc5..afb7b9ee0d5cf6214edf55d5a9c9eb53a0ddc7af 100644
--- a/theories/logrel/examples/mapper_list.v
+++ b/theories/logrel/examples/mapper_list.v
@@ -1,14 +1,31 @@
+(** This file contains an example of a client that uses a service
+with the type:
+
+  ? (X,Y:★) (X ⊸ Y). μ rec. & { cont : ?X. !Y. rec,
+                                stop : end }
+
+It does so to map the values of an input list with type
+[list A] using an input function [A → B], into a list with
+type [list B].
+
+The client cannot be type checked with the rules of the type system,
+as its behaviour depends on the length of the list.
+Its typing judgement can however be manually verified, after which
+it is composed with the type checked service. *)
 From actris.channel Require Import proofmode proto channel.
 From actris.logrel Require Import session_types subtyping_rules
      term_typing_judgment term_typing_rules session_typing_rules
      environments telescopes napp.
 From actris.utils Require Import llist.
-From actris.logrel.lib Require Import par_start.
+From actris.logrel.lib Require Import list par_start.
 From iris.proofmode Require Import tactics.
 
+Definition cont : Z := 1.
+Definition stop : Z := 2.
+
 Definition mapper_service_aux : expr := λ: "f" "c",
   (rec: "go" "f" "c":=
-    (branch [1%Z;2%Z]) "c"
+    (branch [cont;stop]) "c"
     (λ: "c", let: "v" := recv "c" in
      send "c" ("f" "v");; "go" "f" "c")
     (λ: "c", #())) "f" "c".
@@ -21,19 +38,19 @@ Definition mapper_service : expr :=
 Definition send_all : val :=
   rec: "go" "c" "xs" :=
     if: lisnil "xs" then #() else
-      send "c" #1;; send "c" (lpop "xs");; "go" "c" "xs".
+      select "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".
 
 Definition recv_all : val :=
   rec: "go" "c" "ys" "n" :=
     if: "n" = #0 then #() else
       let: "x" := recv "c" in
-      "go" "c" "ys" ("n"-#1);; lcons "x" "ys".
+      "go" "c" "ys" ("n"-#1%Z);; lcons "x" "ys".
 
 Definition mapper_client : expr :=
   (λ: "f" "xs" "c",
    send "c" "f";;
    let: "n" := llength "xs" in
-   send_all "c" "xs";; recv_all "c" "xs" "n";; send "c" #2%Z;; "xs")%E.
+   send_all "c" "xs";; recv_all "c" "xs" "n";; select "c" #stop;; "xs")%E.
 
 Definition mapper_prog : expr :=
   (λ: "f" "xs",
@@ -44,9 +61,8 @@ Section mapper_example.
 
   Definition mapper_type_rec_service_aux (A : ltty Σ) (B : ltty Σ) (rec : lsty Σ)
     : lsty Σ :=
-    lty_branch
-      (<[1%Z := (<??> TY A; <!!> TY B ; rec)%lty]>
-       (<[2%Z := END%lty]>∅)).
+    lty_branch $ <[cont := (<??> TY A; <!!> TY B ; rec)%lty]>
+               $ <[stop := END%lty]> $ ∅.
   Instance mapper_type_rec_service_contractive A B :
     Contractive (mapper_type_rec_service_aux A B).
   Proof. solve_proto_contractive. Qed.
@@ -125,8 +141,8 @@ Section mapper_example.
 
   Definition mapper_type_rec_client_aux
              (A : ltty Σ) (B : ltty Σ) (rec : lsty Σ) : lsty Σ :=
-    lty_select (<[1%Z := (<!!> TY A; <??> TY B ; rec)%lty]>
-                (<[2%Z := END%lty]>∅)).
+    lty_select $ <[cont := (<!!> TY A; <??> TY B ; rec)%lty]>
+               $ <[stop := END%lty]> $ ∅.
   Instance mapper_type_rec_client_contractive A B :
     Contractive (mapper_type_rec_client_aux A B).
   Proof. solve_proto_contractive. Qed.
@@ -138,52 +154,11 @@ Section mapper_example.
                            (mapper_type_rec_client A B))).
   Proof. apply proto_unfold_eq,
          (fixpoint_unfold (mapper_type_rec_client_aux A B)). Qed.
-
   Definition mapper_type_client : lsty Σ :=
     <!! A B> TY A → B ; mapper_type_rec_client A B.
 
-  Definition lty_list_aux (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
-    (() + (A * ref_uniq X))%lty.
-  Instance lty_list_aux_contractive A :
-    Contractive (lty_list_aux A).
-  Proof. solve_proto_contractive. Qed.
-  Definition lty_list (A : ltty Σ) : ltty Σ := lty_rec (lty_list_aux A).
-
-  Notation "'list' A" := (lty_list A) (at level 10) : lty_scope.
-
-  Definition list_pred (A : ltty Σ) : val → val → iProp Σ :=
-    (λ v w : val, ⌜v = w⌝ ∗ ltty_car A v)%I.
-
-  Lemma llength_spec A (l : loc) :
-    ⊢ {{{ ltty_car (ref_uniq (list A)) #l }}} llength #l
-      {{{ xs (n:Z), RET #n; ⌜Z.of_nat (length xs) = n⌝ ∗
-                            llist (λ v w , ⌜v = w⌝ ∗ ltty_car A v) l xs }}}.
-  Proof.
-    iIntros "!>" (Φ) "Hl HΦ".
-    iLöb as "IH" forall (l Φ).
-    iDestruct "Hl" as (ltmp l' [=]) "[Hl Hl']"; rewrite -H2.
-    wp_lam.
-    rewrite {2}/lty_list /lty_rec /lty_list_aux fixpoint_unfold.
-    iDestruct "Hl'" as "[Hl' | Hl']".
-    - iDestruct "Hl'" as (xs ->) "Hl'".
-      wp_load. wp_pures.
-      iAssert (llist (list_pred A) l [])%I with "[Hl Hl']" as "Hl".
-      { rewrite /llist. iDestruct "Hl'" as %->. iApply "Hl". }
-      iApply "HΦ". eauto with iFrame.
-    - iDestruct "Hl'" as (xs ->) "Hl'".
-      wp_load. wp_pures.
-      iDestruct "Hl'" as (x vl' ->) "[HA Hl']".
-      iDestruct "Hl'" as (l' xs ->) "[Hl' Hl'']".
-      wp_apply ("IH" with "[Hl' Hl'']").
-      { iExists _, _. iFrame "Hl' Hl''". done. }
-      iIntros (ys n) "[<- H]".
-      iAssert (llist (list_pred A) l (x :: ys))%I with "[Hl HA H]" as "Hl".
-      { iExists x, l'. eauto with iFrame. }
-      wp_pures. iApply "HΦ". iFrame "Hl". by rewrite (Nat2Z.inj_add 1).
-  Qed.
-
   Definition send_type (A : ltty Σ) : lsty Σ :=
-    (lty_select (<[1%Z := <!!> TY A ; END ]>∅))%lty.
+    (lty_select (<[cont := <!!> TY A ; END ]>∅))%lty.
   Definition recv_type (B : ltty Σ) : lsty Σ :=
     (<??> TY B ; END)%lty.
 
@@ -263,16 +238,17 @@ Section mapper_example.
   Qed.
 
   Lemma send_all_spec_upfront A c l xs ty :
-    {{{ llist (list_pred A) l xs ∗
+    {{{ llist (llist_type_pred A) l xs ∗
         c ↣ lsty_car (lty_napp (send_type A) (length xs) <++> ty) }}}
       send_all c #l
-    {{{ RET #(); llist (list_pred A) l [] ∗ c ↣ lsty_car ty }}}.
+    {{{ RET #(); llist (llist_type_pred A) l [] ∗ c ↣ lsty_car ty }}}.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH".
     { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
       iApply "HΦ". iFrame. }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    rewrite /select.
     wp_send with "[]"; first by eauto.
     rewrite lookup_total_insert.
     wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
@@ -283,10 +259,10 @@ Section mapper_example.
   Qed.
 
   Lemma send_all_spec_aux A B c l xs n :
-    {{{ llist (list_pred A) l xs ∗
+    {{{ llist (llist_type_pred A) l xs ∗
         c ↣ lsty_car (lty_napp (recv_type B) n <++> (mapper_type_rec_client A B)) }}}
       send_all c #l
-    {{{ RET #(); llist (list_pred A) l [] ∗
+    {{{ RET #(); llist (llist_type_pred A) l [] ∗
                  c ↣ lsty_car (lty_napp (recv_type B) (length xs + n) <++>
                                              (mapper_type_rec_client A B)) }}}.
   Proof.
@@ -298,6 +274,7 @@ Section mapper_example.
     simpl.
     iDestruct (iProto_mapsto_le c with "Hc []") as "Hc".
     { iApply recv_mapper_type_rec_client_unfold_app. }
+    rewrite /select.
     wp_send with "[]"; first by eauto.
     rewrite lookup_total_insert.
     wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
@@ -308,10 +285,10 @@ Section mapper_example.
   Qed.
 
   Lemma send_all_spec_ad_hoc A B c l xs :
-    {{{ llist (list_pred A) l xs ∗
+    {{{ llist (llist_type_pred A) l xs ∗
         c ↣ lsty_car (mapper_type_rec_client A B) }}}
       send_all c #l
-    {{{ RET #(); llist (list_pred A) l [] ∗
+    {{{ RET #(); llist (llist_type_pred A) l [] ∗
                  c ↣ lsty_car (lty_napp (recv_type B) (length xs)
                                              <++> (mapper_type_rec_client A B)) }}}.
   Proof.
@@ -323,11 +300,11 @@ Section mapper_example.
   Qed.
 
   Lemma recv_all_spec B c ty l n :
-    {{{ llist (list_pred B) l [] ∗
+    {{{ llist (llist_type_pred B) l [] ∗
               c ↣ lsty_car (lty_napp (recv_type B) n <++> ty) }}}
       recv_all c #l #n
     {{{ ys, RET #(); ⌜n = length ys⌝ ∗
-                     llist (list_pred B) l ys ∗ c ↣ lsty_car ty }}}.
+                     llist (llist_type_pred B) l ys ∗ c ↣ lsty_car ty }}}.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iLöb as "IH" forall (n Φ).
@@ -343,11 +320,11 @@ Section mapper_example.
     iPureIntro. by rewrite H1.
   Qed.
 
-    Lemma ltyped_mapper_client_ad_hoc Γ (A B : ltty Σ) :
+  Lemma ltyped_mapper_client_ad_hoc Γ (A B : ltty Σ) :
     ⊢ Γ ⊨ mapper_client : (A → B) ⊸
-                          ref_uniq (lty_list A) ⊸
+                          lty_list A ⊸
                           chan mapper_type_client ⊸
-                          ref_uniq (lty_list B).
+                          lty_list B.
   Proof.
     iApply (ltyped_lam []).
     iApply (ltyped_lam [EnvItem "f" _]).
@@ -360,9 +337,8 @@ Section mapper_example.
     iDestruct (env_ltyped_cons _ _ "xs" with "HΓ") as (vl ->) "[Hl HΓ]".
     iDestruct (env_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
     wp_send with "[Hf//]".
-    iDestruct "Hl" as (l' v ->) "[Hl Hv]".
-    wp_apply (llength_spec with "[Hl Hv]").
-    { iExists l', v. eauto with iFrame. }
+    iDestruct (list_type_loc with "Hl") as %[l ->].
+    wp_apply (llength_spec A with "Hl").
     iIntros (xs n) "[<- Hl]".
     wp_pures.
     wp_apply (send_all_spec_ad_hoc with "[$Hl $Hc]").
@@ -370,33 +346,18 @@ Section mapper_example.
     wp_apply (recv_all_spec with "[Hl $Hc //]").
     iIntros (ys). iDestruct 1 as (Hlen) "[Hl Hc]".
     rewrite /mapper_type_rec_client /lty_rec fixpoint_unfold.
+    rewrite /select.
     wp_send with "[]"; first by eauto.
     wp_pures.
     iFrame.
-    rewrite /lty_list.
-    iRevert (Hlen).
-    iInduction ys as [|y ys] "IH" forall (l' xs); iIntros (Hlen).
-    - iExists l', NONEV. rewrite /llist. iFrame "Hl".
-      iSplit=> //.
-      rewrite /lty_rec. rewrite (fixpoint_unfold (lty_list_aux B)).
-      iLeft. eauto.
-    - iDestruct "Hl" as (vb l'') "[[-> HB] [Hl' Hrec]]".
-      iExists l', _.
-      iFrame "Hl'".
-      iSplit=> //.
-      rewrite /lty_rec.
-      rewrite {2}(fixpoint_unfold (lty_list_aux B)).
-      iRight. iExists _. iSplit=> //.
-      iExists _, _.
-      iSplit=> //.
-      iFrame "HB". by iApply ("IH" with "Hrec Hc").
+    by iApply llist_lty_list.
   Qed.
 
   Lemma ltyped_mapper_client_upfront Γ (A B : ltty Σ) :
     ⊢ Γ ⊨ mapper_client : (A → B) ⊸
-                          ref_uniq (lty_list A) ⊸
+                          lty_list A ⊸
                           chan mapper_type_client ⊸
-                          ref_uniq (lty_list B).
+                          lty_list B.
   Proof.
     iApply (ltyped_lam []).
     iApply (ltyped_lam [EnvItem "f" _]).
@@ -409,9 +370,8 @@ Section mapper_example.
     iDestruct (env_ltyped_cons _ _ "xs" with "HΓ") as (vl ->) "[Hl HΓ]".
     iDestruct (env_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
     wp_send with "[Hf//]".
-    iDestruct "Hl" as (l' v ->) "[Hl Hv]".
-    wp_apply (llength_spec with "[Hl Hv]").
-    { iExists l', v. eauto with iFrame. }
+    iDestruct (list_type_loc with "Hl") as %[l ->].
+    wp_apply (llength_spec with "Hl").
     iIntros (xs n) "[<- Hl]".
     wp_pures.
     iDestruct (iProto_mapsto_le vc with "Hc []") as "Hc".
@@ -421,25 +381,11 @@ Section mapper_example.
     wp_apply (recv_all_spec with "[Hl $Hc //]").
     iIntros (ys). iDestruct 1 as (Hlen) "[Hl Hc]".
     rewrite /mapper_type_rec_client /lty_rec fixpoint_unfold.
+    rewrite /select.
     wp_send with "[]"; first by eauto.
     wp_pures.
     iFrame.
-    rewrite /lty_list.
-    iRevert (Hlen).
-    iInduction ys as [|y ys] "IH" forall (l' xs); iIntros (Hlen).
-    - iExists l', NONEV. rewrite /llist. iFrame "Hl".
-      iSplit=> //.
-      rewrite /lty_rec. rewrite (fixpoint_unfold (lty_list_aux B)).
-      iLeft. eauto.
-    - iDestruct "Hl" as (vb l'') "[[-> HB] [Hl' Hrec]]".
-      iExists l', _.
-      iFrame "Hl'".
-      iSplit=> //.
-      rewrite /lty_rec {2}(fixpoint_unfold (lty_list_aux B)).
-      iRight. iExists _. iSplit=> //.
-      iExists _, _.
-      iSplit=> //.
-      iFrame "HB". by iApply ("IH" with "Hrec Hc").
+    by iApply llist_lty_list.
   Qed.
 
   Lemma lty_le_mapper_type_client_dual :
@@ -469,10 +415,10 @@ Section mapper_example.
     Context `{!spawnG Σ}.
 
     Lemma ltyped_mapper_prog A B e1 e2 Γ Γ' Γ'' :
-      (Γ ⊨ e2 : ref_uniq (lty_list A) ⫤ Γ') -∗
+      (Γ ⊨ e2 : lty_list A ⫤ Γ') -∗
       (Γ' ⊨ e1 : (A → B) ⫤ Γ'') -∗
       Γ ⊨ par_start (mapper_service) (mapper_client e1 e2) :
-        (() * (ref_uniq (lty_list B))) ⫤ Γ''.
+        (() * lty_list B) ⫤ Γ''.
     Proof.
       iIntros "He2 He1".
       iApply (ltyped_app with "[He2 He1]").
diff --git a/theories/logrel/lib/list.v b/theories/logrel/lib/list.v
new file mode 100644
index 0000000000000000000000000000000000000000..e33563a7fc5017e0a933f1b697a011c5d04974c4
--- /dev/null
+++ b/theories/logrel/lib/list.v
@@ -0,0 +1,75 @@
+From actris.utils Require Import llist.
+From actris.channel Require Import proofmode.
+From actris.logrel Require Import term_types.
+
+Definition lty_list_aux `{!heapG Σ} (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
+  ref_uniq (() + (A * X)).
+Instance lty_list_aux_contractive `{!heapG Σ} A :
+  Contractive (@lty_list_aux Σ _ A).
+Proof. solve_proto_contractive. Qed.
+Definition lty_list `{!heapG Σ} (A : ltty Σ) : ltty Σ := lty_rec (lty_list_aux A).
+
+Notation "'list' A" := (lty_list A) (at level 10) : lty_scope.
+
+Section with_Σ.
+  Context `{!heapG Σ}.
+
+  Lemma list_type_loc A v :
+    ltty_car (list A) v -∗ ∃ (l : loc) , ⌜v = #l⌝.
+  Proof.
+    iIntros "Hv". rewrite /lty_list /lty_rec fixpoint_unfold.
+    iDestruct "Hv" as (l v' Heq) "Hv". by iExists l.
+  Qed.
+
+  Definition llist_type_pred (A : ltty Σ) : val → val → iProp Σ :=
+    (λ v w : val, ⌜v = w⌝ ∗ ltty_car A v)%I.
+
+  Lemma llist_lty_list lys ys A :
+    llist (llist_type_pred A) lys ys -∗
+          ltty_car (lty_list A) #lys.
+  Proof.
+    iIntros "Hlys".
+    iInduction ys as [|y ys] "IH" forall (lys).
+    - rewrite /lty_list /lty_rec fixpoint_unfold.
+      iExists lys, NONEV. rewrite /llist. iFrame "Hlys".
+      iSplit; [ done | ].
+      iLeft. eauto.
+    - iDestruct "Hlys" as (vb l'') "[[-> HB] [Hl' Hrec]]".
+      iEval (rewrite /lty_list /lty_rec fixpoint_unfold).
+      iExists lys, _. iFrame "Hl'".
+      iSplit; [ done | ].
+      rewrite /lty_list /lty_rec.
+      iRight. iExists _. iSplit; [ done | ]. iExists _, _. iSplit; [ done | ].
+      iFrame "HB". by iApply ("IH" with "Hrec").
+  Qed.
+
+  Lemma llength_spec A (l : loc) :
+    ⊢ {{{ ltty_car (list A) #l }}} llength #l
+      {{{ xs (n:Z), RET #n; ⌜Z.of_nat (length xs) = n⌝ ∗
+                            llist (llist_type_pred A) l xs }}}.
+  Proof.
+    iIntros "!>" (Φ) "Hl HΦ".
+    iLöb as "IH" forall (l Φ).
+    wp_lam.
+    rewrite {2}/lty_list /lty_rec /lty_list_aux fixpoint_unfold.
+    iDestruct "Hl" as (ltmp l' [=<-]) "[Hl [ Hl' | Hl' ]]".
+    - wp_load. iDestruct "Hl'" as (xs ->) "Hl'". wp_pures.
+      iAssert (llist (llist_type_pred A) l [])%I with "[Hl Hl']" as "Hl".
+      { rewrite /llist. iDestruct "Hl'" as %->. iApply "Hl". }
+      iApply "HΦ". eauto with iFrame.
+    - wp_load. iDestruct "Hl'" as (xs ->) "Hl'". wp_pures.
+      iDestruct "Hl'" as (x vl' ->) "[HA Hl']".
+      wp_pures.
+      rewrite fixpoint_unfold.
+      iDestruct "Hl'" as (l' xs ->) "[Hl' Hl'']".
+      wp_apply ("IH" with "[Hl' Hl'']").
+      { rewrite /lty_list /lty_rec.
+        iEval (rewrite fixpoint_unfold).
+        iExists _, _. iFrame "Hl' Hl''". done. }
+      iIntros (ys n) "[<- H]".
+      iAssert (llist (llist_type_pred A) l (x :: ys))%I with "[Hl HA H]" as "Hl".
+      { iExists x, l'. eauto with iFrame. }
+      wp_pures. iApply "HΦ". iFrame "Hl". by rewrite (Nat2Z.inj_add 1).
+  Qed.
+
+End with_Σ.