diff --git a/theories/logrel/kind_tele.v b/theories/logrel/kind_tele.v
index 3e4d1860a4237010b65e388c56f188ec06b102d6..2e49662b29df51056d6ef382adc5aaf840d3ac1f 100644
--- a/theories/logrel/kind_tele.v
+++ b/theories/logrel/kind_tele.v
@@ -42,10 +42,11 @@ Inductive ltys {Σ} : ktele Σ → Type :=
   | LTysS {k} {binder} (K : lty Σ k) :
       ltys (binder K) →
       ltys (KTeleS binder).
+Arguments ltys : clear implicits.
 
-Definition ktele_app {Σ} {kt : ktele Σ} {T} (f : kt -k> T) : ltys kt → T :=
-  λ Ks, (fix rec {kt} (Ks : ltys kt) : (kt -k> T) → T :=
-     match Ks in ltys kt return (kt -k> T) → T with
+Definition ktele_app {Σ} {kt : ktele Σ} {T} (f : kt -k> T) : ltys Σ kt → T :=
+  λ Ks, (fix rec {kt} (Ks : ltys Σ kt) : (kt -k> T) → T :=
+     match Ks in ltys _ kt return (kt -k> T) → T with
      | LTysO => λ t : T, t
      | LTysS K Ks => λ f, rec Ks (f K)
      end) kt Ks f.
@@ -56,15 +57,15 @@ Arguments ktele_app {_} {!_ _} _ !_ /.
 (* Local Coercion ktele_app : ktele_fun >-> Funclass. *)
 
 (** Inversion lemma for [tele_arg] *)
-Lemma ltys_inv {Σ} {kt : ktele Σ} (Ks : ltys kt) :
-  match kt as kt return ltys kt → Prop with
+Lemma ltys_inv {Σ} {kt : ktele Σ} (Ks : ltys Σ kt) :
+  match kt as kt return ltys _ kt → Prop with
   | KTeleO => λ Ks, Ks = LTysO
   | KTeleS f => λ Ks, ∃ K Ks', Ks = LTysS K Ks'
   end Ks.
 Proof. induction Ks; eauto. Qed.
-Lemma ltys_O_inv {Σ} (Ks : ltys (@KTeleO Σ)) : Ks = LTysO.
+Lemma ltys_O_inv {Σ} (Ks : ltys Σ (@KTeleO Σ)) : Ks = LTysO.
 Proof. exact (ltys_inv Ks). Qed.
-Lemma ltys_S_inv {Σ} {X} {f : lty Σ X → ktele Σ} (Ks : ltys (KTeleS f)) :
+Lemma ltys_S_inv {Σ} {X} {f : lty Σ X → ktele Σ} (Ks : ltys Σ (KTeleS f)) :
   ∃ K Ks', Ks = LTysS K Ks'.
 Proof. exact (ltys_inv Ks). Qed.
 (*
@@ -93,16 +94,16 @@ Lemma ktele_fmap_app {Σ} {T U} {kt : ktele Σ} (F : T → U) (t : kt -k> T) (x
 Proof. apply ktele_map_app. Qed.
 *)
 (** Operate below [tele_fun]s with argument telescope [kt]. *)
-Fixpoint ktele_bind {Σ} {U} {kt : ktele Σ} : (ltys kt → U) → kt -k> U :=
-  match kt as kt return (ltys kt → U) → kt -k> U with
+Fixpoint ktele_bind {Σ} {U} {kt : ktele Σ} : (ltys Σ kt → U) → kt -k> U :=
+  match kt as kt return (ltys _ kt → U) → kt -k> U with
   | KTeleO => λ F, F LTysO
-  | @KTeleS _ k b => λ (F : ltys (KTeleS b) → U) (K : lty Σ k), (* b x -t> U *)
+  | @KTeleS _ k b => λ (F : ltys Σ (KTeleS b) → U) (K : lty Σ k), (* b x -t> U *)
                   ktele_bind (λ Ks, F (LTysS K Ks))
   end.
 Arguments ktele_bind {_} {_ !_} _ /.
 
 (* Show that tele_app ∘ tele_bind is the identity. *)
-Lemma ktele_app_bind {Σ} {U} {kt : ktele Σ} (f : ltys kt → U) K :
+Lemma ktele_app_bind {Σ} {U} {kt : ktele Σ} (f : ltys Σ kt → U) K :
   ktele_app (ktele_bind f) K = f K.
 Proof.
   induction kt as [|k b IH]; simpl in *.
@@ -117,6 +118,13 @@ Fixpoint ktele_to_tele {Σ} (kt : ktele Σ) : tele :=
   | KTeleS b => TeleS (λ x, ktele_to_tele (b x))
   end.
 
+Fixpoint ltys_to_tele_args {Σ} {kt} (Ks : ltys Σ kt) :
+    tele_arg (ktele_to_tele kt) :=
+  match Ks with
+  | LTysO => TargO
+  | LTysS K Ks => TargS K (ltys_to_tele_args Ks)
+  end.
+
 (*
 
 (** We can define the identity function and composition of the [-t>] function *)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index eecd13a61b4f7ec2770dce7a5a41175e4e704dda..f83f644eefa4e86bb445c402960c1f4652252fb7 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -9,7 +9,7 @@ Bind Scope lmsg_scope with lmsg.
 Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
   (∃ X, M X)%msg.
 
-Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys kt → lmsg Σ) : lmsg Σ :=
+Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) : lmsg Σ :=
   ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M).
 
 Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index db00e0bfe7b37a4b73d742b3722559abf10fc650..1401ea72cdc90d17a8e8ccf87ce707308fb3d546 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -268,21 +268,21 @@ Section subtyping_rules.
   Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
   (* Elimination rules need inhabited variant of telescopes in the model *)
-  Lemma lty_le_texist_elim_l {kt : ktele Σ} (M : ltys kt → lmsg Σ) S :
+  Lemma lty_le_texist_elim_l {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) S :
     (∀ Xs, (<??> M Xs) <: S) -∗
     (<??.. Xs> M Xs) <: S.
   Proof. Admitted.
 
-  Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys kt → lmsg Σ) S :
+  Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) S :
     (∀ Xs, S <: (<!!> M Xs)) -∗
     S <: (<!!.. Xs> M Xs).
   Proof. Admitted.
 
-  Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys kt → lmsg Σ) Ks :
+  Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks :
     ⊢ (<!!.. Xs> M Xs) <: (<!!> M Ks).
   Proof. Admitted.
 
-  Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys kt → lmsg Σ) Ks :
+  Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks :
     ⊢ (<??> M Ks) <: (<??.. Xs> M Xs).
   Proof. Admitted.
 
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 9e09a8c806eca2325f81b5a41ba8333d1327a10c..19c17babf0de1ce93a37f6c60b02d38933c5255d 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -28,7 +28,7 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I.
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
-Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys kt → ltty Σ) : ltty Σ :=
+Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys Σ kt → ltty Σ) : ltty Σ :=
   ktele_fold (@lty_exist Σ) (λ x, x) (ktele_bind C).
 
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index a4f6155b2d636b0169060962e4de99a19fd04ce5..3844ec2a4cdd4e77d601fab6fa9ac27995b64ccb 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -258,11 +258,11 @@ Section properties.
     iApply env_ltyped_delete=> //.
   Qed.
 
-  Lemma texist_exist {kt : ktele Σ} (C : ltys kt → ltty Σ) v :
+  Lemma texist_exist {kt : ktele Σ} (C : ltys Σ kt → ltty Σ) v :
     ltty_car (lty_texist C) v -∗ (∃ X, ▷ ltty_car (C X) v).
   Proof. Admitted.
 
-  Lemma ltyped_unpack' {kt} Γ1 Γ2 Γ3 x e1 e2 (C : ltys kt → ltty Σ) B :
+  Lemma ltyped_unpack' {kt} Γ1 Γ2 Γ3 x e1 e2 (C : ltys Σ kt → ltty Σ) B :
       (Γ1 ⊨ e1 : lty_texist C ⫤ Γ2) -∗
       (∀ Ys, binder_insert x (C Ys) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
       Γ1 ⊨ (let: x := e1 in e2) : B ⫤ binder_delete x Γ3.
@@ -487,6 +487,10 @@ Section properties.
   Section with_chan.
     Context `{chanG Σ}.
 
+    Lemma chan_texist_exist {kt : ktele Σ} c (M : ktele_to_tele kt → lmsg Σ) :
+      ltty_car (chan (<??.. Xs> M (ltys_to_tele_args Xs) )) c -∗ c ↣ (<?.. Xs> M Xs).
+    Proof. Admitted.
+
     Definition chanalloc : val := λ: "u", let: "cc" := new_chan #() in "cc".
     Lemma ltyped_chanalloc S :
       ⊢ ∅ ⊨ chanalloc : () → (chan S * chan (lty_dual S)).
@@ -539,7 +543,7 @@ Section properties.
     Qed.
 
     Lemma ltyped_recv_poly {kt : ktele Σ} Γ1 Γ2 (c : string) (x : string) (e : expr)
-          (A : ltys kt → ltty Σ) (S : ltys kt → lsty Σ) (B : ltty Σ) :
+          (A : ltys Σ kt → ltty Σ) (S : ltys Σ kt → lsty Σ) (B : ltty Σ) :
       ⊢ (∀ Ys, binder_insert x (A Ys) (<[c := (chan (S Ys))%lty ]> Γ1) ⊨ e : B ⫤ Γ2) -∗
         <[c := (chan (<??> ∃.. Xs, TY A Xs; S Xs))%lty]> Γ1 ⊨
           (let: x := recv c in e) : B ⫤ binder_delete x Γ2.
@@ -549,6 +553,8 @@ Section properties.
       { by apply lookup_insert. }
       rewrite Heq.
       rewrite delete_insert; last by admit.
+      iDestruct (chan_texist_exist v' with "[Hc]") as "Hc".
+      { admit. }
       wp_apply (recv_spec with "[Hc]").
       { admit. }
       iIntros (Xs) "[Hc HC]".