diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index ded8b10d35d2992cc482e4efd175a0619924670a..c74adeb2e2a397d3f1162ea6d6b832e3590aad16 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -95,6 +95,7 @@ Section double.
   Proof.
     iIntros (vs) "!> HΓ /=".
     iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros (c) "Hc".
     iApply (wp_prog with "[Hc]").
     { iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
index b2621b3dd5d756e7265a8f2375e1f92ec9e438e3..21b97d2a2156b15b906ca31d7102cbd158810b71 100755
--- a/theories/logrel/ltyping.v
+++ b/theories/logrel/ltyping.v
@@ -112,6 +112,17 @@ Section Environment.
     rewrite /env_split. rewrite /env_ltyped.
   Admitted.
 
+  Lemma env_split_id_l Γ : ⊢ env_split Γ ∅ Γ.
+  Proof.
+    iIntros "!>" (vs).
+    iSplit; [iIntros "$" | iIntros "[_ $]"]; iApply env_ltyped_empty.
+  Qed.
+  Lemma env_split_id_r Γ : ⊢ env_split Γ Γ ∅.
+  Proof.
+    iIntros "!>" (vs).
+    iSplit; [iIntros "$" | iIntros "[$ _]"]; iApply env_ltyped_empty.
+  Qed.
+
   Lemma env_split_empty : ⊢ env_split ∅ ∅ ∅.
   Proof.
     iIntros "!>" (vs).
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 6fe83188344759ad9ce09aaefc8634feaa59b3db..a89932b08007349cc0eb9197816396c8ece2218e 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -481,13 +481,13 @@ Section subtype.
     iApply (iProto_mapsto_le with "H [Hle]"). eauto.
   Qed.
 
-  Theorem ltyped_subsumption Γ e τ1 τ2 :
-    τ1 <: τ2 -∗ (Γ ⊨ e : τ1) -∗ (Γ ⊨ e : τ2).
+  Theorem ltyped_subsumption Γ Γ2 e τ1 τ2 :
+    τ1 <: τ2 -∗ (Γ ⊨ e : τ1 ⫤ Γ2) -∗ (Γ ⊨ e : τ2 ⫤ Γ2).
   Proof.
     iIntros "#Hle #Hltyped" (vs) "!> Henv".
     iDestruct ("Hltyped" with "Henv") as "Hltyped'".
     iApply (wp_wand with "Hltyped' [Hle]").
-    by iIntros (v).
+    iIntros (v) "[H1 $]". by iApply "Hle".
   Qed.
 
 End subtype.
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index bce95ea0a19b2abe47158956a4bc2b2f5a91a203..37ae72190748f928fb0dfa6b40b2c061fe84c182 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -79,9 +79,6 @@ Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
 Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : lty_scope.
 Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
 
-Instance binder_insert_instance : Insert binder A (gmap string A) :=
-  { insert := binder_insert }.
-
 Section properties.
   Context `{heapG Σ}.
   Implicit Types Γ : gmap string (lty Σ).
@@ -190,47 +187,52 @@ Section properties.
     iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
   Qed.
 
-  Lemma ltyped_lam Γ Γ1 Γ2 x e A1 A2 :
-    (<[ x := A1 ]>Γ ⊨ e : A2 ⫤ Γ2) -∗
-    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ binder_delete x Γ2.
+  Lemma ltyped_lam Γ Γ' x e A1 A2 :
+    (binder_insert x A1 Γ ⊨ e : A2 ⫤ Γ') -∗
+    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ ∅.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
     wp_pures.
-    iSplitL; last by admit.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros (v) "HA1". wp_pures.
     iDestruct ("He" $!((binder_insert x v vs)) with "[HA1 HΓ]") as "He'".
     { iApply (env_ltyped_insert with "[HA1 //] HΓ"). }
-    rewrite -subst_map_binder_insert.
-    iApply (wp_wand with "He'").
-    iIntros (w) "[$ _]".
-  Admitted.
+    iDestruct (wp_wand _ _ _ _ (λ v, A2 v) with "He' []") as "He'".
+    { iIntros (w) "[$ _]". }
+    destruct x as [|x]; rewrite /= -?subst_map_insert //.
+  Qed.
 
   Lemma ltyped_let Γ1 Γ2 Γ3 (x : binder) e1 e2 A1 A2 :
-    (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗ (<[x:=A1]>Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ binder_delete x Γ3.
+    (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗ (binder_insert x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
+    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ∅.
   Proof.
     iIntros "#He1 #He2".
-    iApply ltyped_app=> //.    
-    iApply (ltyped_lam)=> //.
+    iApply ltyped_app=> //.
+    iApply (ltyped_frame _ _ _ _ ∅); last by iApply (ltyped_lam).
+    - iApply env_split_id_r.
+    - iApply env_split_empty.
   Qed.
 
   Lemma ltyped_rec Γ Γ' f x e A1 A2 :
     env_copy Γ Γ' -∗
-    (<[f:=(A1 → A2)%lty]>(<[x:=A1]>Γ') ⊨ e : A2) -∗
-    Γ ⊨ (rec: f x := e) : A1 → A2.
+    (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ') ⊨ e : A2) -∗
+    Γ ⊨ (rec: f x := e) : A1 → A2 ⫤ ∅.
   Proof.
     iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
     iDestruct ("Hcopy" with "HΓ") as "HΓ".
     iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
-    iModIntro. iLöb as "IH".
+    iModIntro. iSplitL; last by iApply env_ltyped_empty.
+    iLöb as "IH".
     iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
     iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
                   with "[HΓ HA1]") as "He'".
     { iApply (env_ltyped_insert with "IH").
       iApply (env_ltyped_insert with "HA1 HΓ"). }
+    iDestruct (wp_wand _ _ _ _ (λ v, A2 v) with "He' []") as "He'".
+    { iIntros (w) "[$ _]". }
     destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
     destruct (decide (x = f)) as [->|].
-    - by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
+    - by rewrite subst_subst delete_idemp !insert_insert -subst_map_insert.
     - rewrite subst_subst_ne // -subst_map_insert.
       by rewrite -delete_insert_ne // -subst_map_insert.
   Qed.
@@ -302,6 +304,7 @@ Section properties.
     ⊢ ∅ ⊨ split : A1 * A2 → (A1 ⊸ A2 ⊸ B) ⊸ B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v) "Hv". rewrite /split. wp_pures.
     iDestruct "Hv" as (w1 w2 ->) "[Hw1 Hw2]".
     iIntros (f) "Hf". wp_pures.
@@ -324,7 +327,7 @@ Section properties.
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(HA [HΓ //])").
-    iIntros (v) "HA'". wp_pures.
+    iIntros (v) "[HA' $]". wp_pures.
     iLeft. iExists v. auto.
   Qed.
 
@@ -333,7 +336,7 @@ Section properties.
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(HA [HΓ //])").
-    iIntros (v) "HA'". wp_pures.
+    iIntros (v) "[HA' $]". wp_pures.
     iRight. iExists v. auto.
   Qed.
 
@@ -344,6 +347,7 @@ Section properties.
     ⊢ ∅ ⊨ paircase : A1 + A2 → (A1 ⊸ B) ⊸ (A2 ⊸ B) ⊸ B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     rewrite /paircase. iIntros "!>" (p) "Hp". wp_pures.
     iIntros (f_left) "Hleft". wp_pures.
     iIntros (f_right) "Hright". wp_pures.
@@ -380,31 +384,34 @@ Section properties.
   Qed.
 
   Lemma ltyped_tlam Γ e C :
-    (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (λ: <>, e) : ∀ A, C A.
+    (∀ A, Γ ⊨ e : C A ⫤ ∅) -∗ Γ ⊨ (λ: <>, e) : ∀ A, C A ⫤ ∅.
   Proof.
-    iIntros "#He" (vs) "!> HΓ /=". wp_pures. iIntros (A) "/=". wp_pures.
-    iApply ("He" $!(_ vs) with "HΓ").
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    iSplitL; last by iApply env_ltyped_empty.
+    iIntros (A) "/=". wp_pures.
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
   Qed.
   Lemma ltyped_tlam_lsty Γ e C :
-    (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (λ: <>, e) : ∀p A, C A.
+    (∀ A, Γ ⊨ e : C A ⫤ ∅) -∗ Γ ⊨ (λ: <>, e) : ∀p A, C A ⫤ ∅.
   Proof.
-    iIntros "#He" (vs) "!> HΓ /=". wp_pures. iIntros (A) "/=". wp_pures.
-    iApply ("He" $!(_ vs) with "HΓ").
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    iSplitL; last by iApply env_ltyped_empty.
+    iIntros (A) "/=". wp_pures.
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
   Qed.
 
-  Lemma ltyped_tapp Γ e C A :
-    (Γ ⊨ e : ∀ A, C A) -∗ Γ ⊨ e #() : C A.
+  Lemma ltyped_tapp Γ Γ2 e C A :
+    (Γ ⊨ e : ∀ A, C A ⫤ Γ2) -∗ Γ ⊨ e #() : C A ⫤ Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB".
-    by iApply ("HB" $! A).
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ]".
+    by iApply (wp_wand with "HB [HΓ]"); iIntros (v) "$ //".
   Qed.
-  Lemma ltyped_tapp_lsty Γ e C A :
-    (Γ ⊨ e : ∀p A, C A) -∗ Γ ⊨ e #() : C A.
-  Proof.
+  Lemma ltyped_tapp_lsty Γ Γ2 e C A :
+    (Γ ⊨ e : ∀p A, C A ⫤ Γ2) -∗ Γ ⊨ e #() : C A ⫤ Γ2.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB".
-    by iApply ("HB" $! A).
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ]".
+    by iApply (wp_wand with "HB [HΓ]"); iIntros (v) "$ //".
   Qed.
 
   (** Existential properties *)
@@ -434,13 +441,13 @@ Section properties.
     (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃ A, C A.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB". by iExists A.
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists A.
   Qed.
   Lemma ltyped_pack_lsty Γ e C A :
     (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃p A, C A.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB". by iExists A.
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists A.
   Qed.
 
   Definition unpack : val := λ: "exist" "f", "f" #() "exist".
@@ -449,6 +456,7 @@ Section properties.
     ⊢ ∅ ⊨ unpack : (∃ A, C A) → (∀ A, C A ⊸ B) ⊸ B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v). iDestruct 1 as (A) "Hv".
     rewrite /unpack. wp_pures.
     iIntros (fty) "Hfty". wp_pures.
@@ -462,6 +470,7 @@ Section properties.
     ⊢ ∅ ⊨ unpack : (∃p A, C A) → (∀p A, C A ⊸ B) ⊸ B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v). iDestruct 1 as (A) "Hv".
     rewrite /unpack. wp_pures.
     iIntros (fty) "Hfty". wp_pures.
@@ -485,6 +494,7 @@ Section properties.
     ⊢ ∅ ⊨ alloc : A → ref_mut A.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v) "Hv". rewrite /alloc. wp_pures.
     wp_alloc l as "Hl".
     iExists l, v. iSplit=> //.
@@ -501,6 +511,7 @@ Section properties.
     ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut any.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
     iDestruct "Hv" as (l w ->) "[Hl Hw]".
     wp_load. wp_pures.
@@ -514,6 +525,7 @@ Section properties.
   Proof.
     iIntros (vs) "!> HΓ /=".
     iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
     iDestruct "Hv" as (l w ->) "[Hl #Hw]".
     wp_load. wp_pures.
@@ -528,6 +540,7 @@ Section properties.
     ⊢ ∅ ⊨ store : ref_mut A → B ⊸ ref_mut B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
     iIntros "!>" (v) "Hv". rewrite /store. wp_pures.
     iDestruct "Hv" as (l old ->) "[Hl Hold]".
     iIntros (new) "Hnew". wp_store.
@@ -548,7 +561,9 @@ Section properties.
   Lemma ltyped_fetch_and_add :
     ⊢ ∅ ⊨ fetch_and_add : ref_shr lty_int → lty_int → lty_int.
   Proof.
-    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
+    iIntros (vs) "!> _ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
+    iIntros "!>" (r) "Hr".
     iApply wp_fupd. rewrite /fetch_and_add; wp_pures.
     iDestruct "Hr" as (l ->) "Hr".
     iMod (fupd_mask_mono with "Hr") as "#Hr"; first done.
@@ -564,7 +579,9 @@ Section properties.
   Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} :
     ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A).
   Proof.
-    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
+    iIntros (vs) "!> _ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
+    iIntros "!>" (r) "Hr".
     iApply wp_fupd. rewrite /load; wp_pures.
     iDestruct "Hr" as (l ->) "Hr".
     iMod (fupd_mask_mono with "Hr") as "#Hr"; first done.
@@ -585,7 +602,9 @@ Section properties.
   Lemma ltyped_ref_shrstore (A : lty Σ) :
     ⊢ ∅ ⊨ store : ref_shr A → A → ref_shr A.
   Proof.
-    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
+    iIntros (vs) "!> _ /=". iApply wp_value.
+    iSplitL; last by iApply env_ltyped_empty.
+    iIntros "!>" (r) "Hr".
     iApply wp_fupd. rewrite /store; wp_pures.
     iDestruct "Hr" as (l ->) "#Hr".
     iIntros "!> !>" (x) "HA". wp_pures.
@@ -615,6 +634,7 @@ Section properties.
       ⊢ ∅ ⊨ mutexalloc : A → mutex A.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (v) "Hv". rewrite /mutexalloc. wp_pures.
       wp_alloc l as "Hl".
       wp_bind (newlock _).
@@ -631,6 +651,7 @@ Section properties.
       ⊢ ∅ ⊨ mutexacquire : mutex A → A * mutexguard A.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (m) "Hm". rewrite /mutexacquire. wp_pures.
       iDestruct "Hm" as (γ l lk ->) "Hlock".
       iMod (fupd_mask_mono with "Hlock") as "#Hlock"; first done.
@@ -652,6 +673,7 @@ Section properties.
       ⊢ ∅ ⊨ mutexrelease : A → mutexguard A ⊸ mutex A.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (w1) "Hw1". rewrite /mutexrelease. wp_pures.
       iIntros (w2) "Hw2". wp_pures.
       iDestruct "Hw2" as (γ l lk inner ->) "[#Hlock [Hlocked Hinner]]".
@@ -679,6 +701,7 @@ Section properties.
       ⊢ ∅ ⊨ parallel : (() ⊸ A) → (() ⊸ B) ⊸ (A * B).
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (fa) "Hfa". rewrite /parallel. wp_pures.
       iIntros (fb) "Hfb". wp_pures.
       wp_apply (par_spec A B with "[Hfa] [Hfb]").
@@ -699,6 +722,7 @@ Section properties.
       ⊢ ∅ ⊨ chanalloc : () → (chan S * chan (lsty_dual S)).
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (u) ">->". rewrite /chanalloc. wp_pures.
       wp_apply (new_chan_spec with "[//]"); iIntros (c1 c2) "Hp".
       iDestruct "Hp" as "[Hp1 Hp2]". wp_pures.
@@ -710,21 +734,53 @@ Section properties.
       ⊢ ∅ ⊨ chansend : chan (<!!> A; S) → A ⊸ chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (c) "Hc". rewrite /chansend. wp_pures.
       iIntros (w) "Hw". wp_pures.
       wp_send with "[$Hw]". wp_pures. iFrame "Hc".
     Qed.
 
+    Lemma ltyped_send Γ Γ' (x : string) e A S :
+      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> A; S))%lty]> Γ') -∗
+      Γ ⊨ send x e : () ⫤ <[x:=(chan S)%lty]> Γ'.
+    Proof.
+      iIntros "#He !>" (vs) "HΓ"=> /=.
+      wp_bind (subst_map vs e).
+      iApply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
+      iDestruct (env_ltyped_lookup with "HΓ'") as (v' Heq) "[Hc HΓ']".
+      { by apply lookup_insert. }
+      rewrite Heq.
+      wp_send with "[HA //]".
+      iSplitR; first done.
+      iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ'")
+        as "HΓ'"=> /=.
+      by rewrite insert_delete insert_insert (insert_id vs).
+    Qed.
+
     Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
     Lemma ltyped_chanrecv A S :
       ⊢ ∅ ⊨ chanrecv : chan (<??> A; S) → A * chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
       iIntros "!>" (c) "Hc". rewrite /chanrecv. wp_pures.
       wp_recv (v) as "HA". wp_pures.
       iExists v, c. eauto with iFrame.
     Qed.
 
+    Lemma ltyped_recv Γ (x : string) A S :
+      ⊢ <[x := (chan (<??> A; S))%lty]>Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
+    Proof.
+      iIntros "!>" (vs) "HΓ"=> /=.
+      iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
+      { by apply lookup_insert. }
+      rewrite Heq.
+      wp_recv (v) as "HA".
+      iSplitL "HA"; first done.
+      iDestruct (env_ltyped_insert _ _ x (chan _) _ with "[Hc //] HΓ") as "HΓ"=> /=.
+      by rewrite insert_delete !insert_insert (insert_id vs).
+    Qed.
+
     Definition chanselect : val := λ: "c" "i", send "c" "i";; "c".
     Lemma ltyped_chanselect Γ (c : val) (i : Z) S Ss :
       Ss !! i = Some S →
@@ -734,10 +790,10 @@ Section properties.
       iIntros (Hin) "#Hc !>".
       iIntros (vs) "H /=".
       rewrite /chanselect.
-      iMod (wp_value_inv with "(Hc H)") as "Hc'".
+      iMod (wp_value_inv with "(Hc H)") as "[Hc' HΓ]".
       wp_send with "[]"; [by eauto|].
       rewrite (lookup_total_correct Ss i S)=> //.
-      by wp_pures.
+      wp_pures. iFrame.
     Qed.
 
     Definition chanbranch (xs : list Z) : val := λ: "c",
@@ -751,7 +807,9 @@ Section properties.
         lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A.
     Proof.
       iIntros (Hdom) "!>". iIntros (vs) "Hvs".
-      iApply wp_value. iIntros (c) "Hc". wp_lam.
+      iApply wp_value.
+      iSplitL; last by iApply env_ltyped_empty.
+      iIntros (c) "Hc". wp_lam.
       rewrite -subst_map_singleton.
       iApply lty_arr_list_spec.
       { by rewrite fmap_length. }