diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 15f27ce04ade4826d00b31fbb8b03c51874001e7..ae4faffbd5cec07dd92a123ef37dc9b7c09ae5a0 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -28,8 +28,8 @@ Section fundamental.
     try rel_pure_l; try rel_pure_r; rel_values.
 
   Local Tactic Notation "rel_bind_ap" uconstr(e1) uconstr(e2) constr(IH) ident(v) ident(w) constr(Hv):=
-    rel_bind_l (_ e1);
-    rel_bind_r (_ e2);
+    rel_bind_l (subst_map _ e1);
+    rel_bind_r (subst_map _ e2);
     try iSpecialize (IH with "Hvs");
     iApply (refines_bind with IH);
     iIntros (v w) Hv; simpl.
@@ -482,21 +482,31 @@ Section fundamental.
     iModIntro. by iExists Ï„i.
   Qed.
 
-(*
-  Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2 :
+  Lemma bin_log_related_unpack Δ Γ x e1 e1' e2 e2' τ τ2 :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ) -∗
     (∀ τi : lty2 Σ,
-      {τi::Δ;⤉Γ} ⊨
-        e2 ≤log≤ e2' : TArrow τ (subst (ren (+1)) τ2)) -∗
-    {Δ;Γ} ⊨ unpack e1 e2 ≤log≤ unpack e1' e2' : τ2.
+      {τi::Δ;<[x:=τ]>(⤉Γ)} ⊨
+        e2 ≤log≤ e2' : (subst (ren (+1)) τ2)) -∗
+    {Δ;Γ} ⊨ (unpack: x := e1 in e2) ≤log≤ (unpack: x := e1' in e2') : τ2.
   Proof.
     iIntros "IH1 IH2".
     intro_clause.
-    Abort.
-    iSpecialize ("IH2" $! vs with "[Hvs]").
-    { by rewrite interp_ren. }
-    rel_bind_ap e2 e2' "IH2" v v' "#IH2".
-*)
+    rel_pure_l. rel_pure_r.
+    rel_bind_ap e1 e1' "IH1" v v' "#IH1".
+    iDestruct "IH1" as (A) "#IH".
+    unlock unpack.
+    rel_pure_l. rel_pure_l. rel_pure_l.
+    rel_pure_r. rel_pure_r. rel_pure_r.
+    rel_pure_l. rel_pure_r.
+    iSpecialize ("IH2" $! A (binder_insert x (v,v') vs) with "[Hvs]").
+    { rewrite -(interp_ren A).
+      rewrite binder_insert_fmap.
+      iApply (env_ltyped2_insert with "IH Hvs"). }
+    rewrite !binder_insert_fmap !subst_map_binder_insert /=.
+    iApply (refines_wand with "IH2").
+    iIntros (v1 v2). rewrite (interp_ren_up [] Δ τ2 A).
+    asimpl. eauto.
+  Qed.
 
   Theorem binary_fundamental Δ Γ e τ :
     Γ ⊢ₜ e : τ → ({Δ;Γ} ⊨ e ≤log≤ e : τ)%I.
@@ -523,7 +533,7 @@ Section fundamental.
     - by iApply bin_log_related_fold.
     - by iApply bin_log_related_unfold.
     - by iApply bin_log_related_pack'.
-    (* - iApply (bin_log_related_unpack with "[]"); eauto. *)
+    - iApply (bin_log_related_unpack with "[]"); eauto.
     - by iApply bin_log_related_fork.
     - by iApply bin_log_related_alloc.
     - by iApply bin_log_related_load.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 271b1d61474e07f1c65c8ad5d58b1ac379ccf349..ecce2767f4d1228f8e3ed67bd6e40a795a956c21 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -90,10 +90,6 @@ Section semtypes.
   Qed.
 End semtypes.
 
-(* Shift all the indices in the context by one,
-   used when inserting a new type interpretation in Δ. *)
-Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
-
 Notation "∀ A1 .. An , C" :=
   (lty2_forall (λ A1, .. (lty2_forall (λ An, C%lty2)) ..)) : lty_scope.
 
diff --git a/theories/typing/types.v b/theories/typing/types.v
index d227fdcd019a8a09567983d328989eae9dd1bfcf..8118cce7ecbd2940c79b1170adb43fb2c6832498 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -73,6 +73,10 @@ Notation "'ref' Ï„" := (Tref Ï„%F) (at level 30, right associativity): FType_sco
 (** * Typing judgements *)
 Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 
+(* Shift all the indices in the context by one,
+   used when inserting a new type interpretation in Δ. *)
+Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
+
 (** We model type-level lambdas and applications as thunks *)
 Notation "Λ: e" := (λ: <>, e)%E (at level 200).
 Notation "'TApp' e" := (App e%E #()%E) (at level 200).
@@ -82,6 +86,14 @@ unfold operator to be the identity function. *)
 Definition rec_unfold : val := λ: "x", "x".
 Definition unpack : val := λ: "x" "y", "y" "x".
 
+Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (Lam x%bind e2%E))
+  (at level 200, x at level 1, e1, e2 at level 200, only parsing,
+   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+
+Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (LamV x%bind e2%E))
+  (at level 200, x at level 1, e1, e2 at level 200, only parsing,
+   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : val_scope.
+
 (** Operation lifts *)
 Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
   binder_insert.
@@ -121,17 +133,17 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
   | App_typed e1 e2 Ï„1 Ï„2 :
      Γ ⊢ₜ e1 : TArrow τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2
   | TLam_typed e Ï„ :
-     subst (ren (+1%nat)) <$> Γ ⊢ₜ e : τ →
+     ⤉ Γ ⊢ₜ e : τ →
      Γ ⊢ₜ (Λ: e) : TForall τ
   | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ →
      Γ ⊢ₜ e #() : τ.[τ'/]
   | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜe : TRec τ
   | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ rec_unfold e : τ.[TRec τ/]
   | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
-  (* todo *)
-  (* | TUnpack e1 e2 τ τ2 : Γ ⊢ₜ e1 : TExists τ → *)
-  (*     (subst (ren (+1%nat)) <$> Γ) ⊢ₜ e2 : TArrow τ (subst (ren (+1%nat)) τ2) → *)
-  (*     Γ ⊢ₜ unpack e1 e2 : τ2 *)
+  | TUnpack e1 x e2 Ï„ Ï„2 :
+      Γ ⊢ₜ e1 : TExists τ →
+      <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (subst (ren (+1%nat)) τ2) →
+      Γ ⊢ₜ (unpack: x := e1 in e2) : τ2
   | TFork e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
   | TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ
   | TLoad e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ