diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
index 45c5c5a518c1b143f6e3875294c706202a60dab3..950fb779debd4f29442277b55597d932373dd38e 100644
--- a/theories/logrel/environments.v
+++ b/theories/logrel/environments.v
@@ -55,6 +55,23 @@ Section env.
     by rewrite -Hw lookup_insert_ne.
   Qed.
 
+  Lemma env_ltyped_delete Γ vs x v :
+    Γ !! x = None ->
+    env_ltyped Γ (<[x := v]>vs) -∗
+    env_ltyped Γ vs.
+  Proof.
+    iIntros (HNone) "HΓ".
+    rewrite /env_ltyped.
+    iApply (big_sepM_impl with "HΓ").
+    iIntros "!>" (k A HSome) "H".
+    iDestruct "H" as (w Heq) "HA".
+    iExists _. iFrame.
+    iPureIntro.
+    destruct (decide (x = k)).
+    - subst. rewrite HNone in HSome. inversion HSome.
+    - by rewrite lookup_insert_ne in Heq.
+  Qed.
+
   Lemma env_split_id_l Γ : ⊢ env_split Γ ∅ Γ.
   Proof.
     iIntros "!>" (vs).
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 4a759e234b4ac08d5b6c6dda95c7adf8c4bdc756..c930f4bb62ad69e38a035122dcfedc2432eaec98 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -92,10 +92,24 @@ Section properties.
       by rewrite -delete_insert_ne // -subst_map_insert.
   Qed.
 
-  Lemma ltyped_let Γ1 Γ2 Γ3 (x : binder) e1 e2 A1 A2 :
-    (Γ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; last done. by iApply ltyped_lam. Qed.
+  (* TODO: We would prefer just Γ3 in the second premise *)
+  Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
+    (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗ (binder_insert x A1 Γ2 ⊨ e2 : A2 ⫤ binder_delete x Γ3) -∗
+    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ binder_delete x Γ3.
+  Proof.
+    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
+    wp_apply (wp_wand with "(He1 HΓ1)").
+    iIntros (v) "[HA1 HΓ2]".
+    wp_pures.
+    iDestruct (env_ltyped_insert _ _ x with "HA1 HΓ2") as "HΓ2".
+    iDestruct ("He2" with "HΓ2") as "He2'". 
+    destruct x as [|x]; rewrite /= -?subst_map_insert //.
+    wp_apply (wp_wand with "He2'").
+    iIntros (w) "[HA2 HΓ3]".
+    iFrame.
+    iApply env_ltyped_delete=> //.
+    apply lookup_delete.
+  Qed.
 
   Fixpoint lty_arr_list (As : list (ltty Σ)) (B : ltty Σ) : ltty Σ :=
     match As with
@@ -227,21 +241,24 @@ Section properties.
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
   Qed.
 
-  Definition unpack : val := λ: "exist" "f", "f" #() "exist".
-
-  Lemma ltyped_unpack k (C : lty Σ k → ltty Σ) B :
-    ⊢ ∅ ⊨ unpack : (∃ M, C M) → (∀ M, C M ⊸ B) ⊸ B.
+  Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
+      (Γ1 ⊨ e1 : lty_exist C ⫤ Γ2) -∗
+      (∀ Y, binder_insert x (C Y) Γ2 ⊨ e2 : B ⫤ binder_delete x Γ3) -∗
+      Γ1 ⊨ (let: x := e1 in e2) : B ⫤ binder_delete x Γ3.
   Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v). iDestruct 1 as (M) "Hv".
-    rewrite /unpack. wp_pures.
-    iIntros (fty) "Hfty". wp_pures.
-    iSpecialize ("Hfty" $! M).
-    wp_bind (fty _). wp_apply (wp_wand with "Hfty").
-    iIntros (f) "Hf".
-    wp_apply (wp_wand with "(Hf [Hv //])").
-    iIntros (w) "HB". iApply "HB".
+    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
+    wp_apply (wp_wand with "(He1 HΓ1)").
+    iIntros (v) "[HC HΓ2]".
+    iDestruct "HC" as (X) "HX".
+    wp_pures.
+    iDestruct (env_ltyped_insert _ _ x with "HX HΓ2") as "HΓ2".
+    iDestruct ("He2" with "HΓ2") as "He2'". 
+    destruct x as [|x]; rewrite /= -?subst_map_insert //.
+    wp_apply (wp_wand with "He2'").
+    iIntros (w) "[HA2 HΓ3]".
+    iFrame.
+    iApply env_ltyped_delete=> //.
+    apply lookup_delete.
   Qed.
 
   (** Mutable Reference properties *)